%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL944_8 : 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 : n019.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:24 AM UTC 2026
% Result : Theorem 147.30s 84.90s
% Output : Refutation 147.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 83
% Syntax : Number of formulae : 192 ( 26 unt; 0 typ; 15 def)
% Number of atoms : 2288 ( 34 equ; 0 cnn)
% Maximal formula atoms : 88 ( 11 avg)
% Number of connectives : 8748 ( 655 ~; 670 |; 85 &;6044 @)
% ( 0 <=>;1294 =>; 0 <=; 0 <~>)
% Maximal formula depth : 127 ( 17 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 60 ( 57 usr; 4 con; 0-6 aty)
% Number of variables : 1537 ( 24 ^;1496 !; 2 ?;1537 :)
% ( 0 !>; 0 ?*; 0 @-; 15 @+)
% 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(r2_decl,type,
r2: '$ki_world' > $o ).
thf(r3_decl,type,
r3: '$ki_world' > $o ).
thf(r4_decl,type,
r4: '$ki_world' > $o ).
thf(r5_decl,type,
r5: '$ki_world' > $o ).
thf(equivalence_1_decl,type,
equivalence_1: '$ki_world' > $o ).
thf(equivalence_2_decl,type,
equivalence_2: '$ki_world' > $o ).
thf(cn2_decl,type,
cn2: '$ki_world' > $o ).
thf(cn1_decl,type,
cn1: '$ki_world' > $o ).
thf(cn3_decl,type,
cn3: '$ki_world' > $o ).
thf(kn2_decl,type,
kn2: '$ki_world' > $o ).
thf(kn1_decl,type,
kn1: '$ki_world' > $o ).
thf(kn3_decl,type,
kn3: '$ki_world' > $o ).
thf(equivalence_3_decl,type,
equivalence_3: '$ki_world' > $o ).
thf(op_implies_or_decl,type,
op_implies_or: '$ki_world' > $o ).
thf(op_and_decl,type,
op_and: '$ki_world' > $o ).
thf(and_2_decl,type,
and_2: '$ki_world' > $o ).
thf(and_3_decl,type,
and_3: '$ki_world' > $o ).
thf(and_1_decl,type,
and_1: '$ki_world' > $o ).
thf(implies_2_decl,type,
implies_2: '$ki_world' > $o ).
thf(implies_3_decl,type,
implies_3: '$ki_world' > $o ).
thf(op_implies_and_decl,type,
op_implies_and: '$ki_world' > $o ).
thf(implies_1_decl,type,
implies_1: '$ki_world' > $o ).
thf(substitution_of_equivalents_decl,type,
substitution_of_equivalents: '$ki_world' > $o ).
thf(op_or_decl,type,
op_or: '$ki_world' > $o ).
thf(modus_tollens_decl,type,
modus_tollens: '$ki_world' > $o ).
thf(or_1_decl,type,
or_1: '$ki_world' > $o ).
thf(or_2_decl,type,
or_2: '$ki_world' > $o ).
thf(or_3_decl,type,
or_3: '$ki_world' > $o ).
thf(op_equiv_decl,type,
op_equiv: '$ki_world' > $o ).
thf(modus_ponens_decl,type,
modus_ponens: '$ki_world' > $o ).
thf(r1_decl,type,
r1: '$ki_world' > $o ).
thf(qmltpeq_decl,type,
qmltpeq: '$ki_world' > $i > $i > $o ).
thf(is_a_theorem_decl,type,
is_a_theorem: '$ki_world' > $i > $o ).
thf(equiv_decl,type,
equiv: $i > $i > $i ).
thf(not_decl,type,
not: $i > $i ).
thf(or_decl,type,
or: $i > $i > $i ).
thf(and_decl,type,
and: $i > $i > $i ).
thf(implies_decl,type,
implies: $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: '$ki_world' ).
thf(sk2_decl,type,
sk2: '$ki_world' > $i ).
thf(sk3_decl,type,
sk3: '$ki_world' > '$ki_world' ).
thf(sk4_decl,type,
sk4: '$ki_world' > '$ki_world' ).
thf(sk5_decl,type,
sk5: '$ki_world' > $i ).
thf(sk6_decl,type,
sk6: '$ki_world' > '$ki_world' ).
thf(sk7_decl,type,
sk7: '$ki_world' > $o ).
thf(sk8_decl,type,
sk8: '$ki_world' > '$ki_world' ).
thf(sk9_decl,type,
sk9: '$ki_world' > $i > '$ki_world' > $i > '$ki_world' > '$ki_world' > '$ki_world' ).
thf(sk10_decl,type,
sk10: '$ki_world' > $i > '$ki_world' > $i > '$ki_world' > '$ki_world' > '$ki_world' ).
thf(sk11_decl,type,
sk11: '$ki_world' > '$ki_world' ).
thf(sk12_decl,type,
sk12: '$ki_world' > $i ).
thf(sk13_decl,type,
sk13: '$ki_world' > '$ki_world' ).
thf(sk14_decl,type,
sk14: '$ki_world' > $i ).
thf(sk15_decl,type,
sk15: '$ki_world' > '$ki_world' ).
thf(sk16_decl,type,
sk16: '$ki_world' > '$ki_world' ).
thf(sk1_def,definition,
( sk1
= ( @+[A: '$ki_world'] :
~ ( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ r2 ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: '$ki_world'] :
@+[B: $i] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r1 ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: '$ki_world'] :
@+[B: $i] :
~ ( ( B @ ( A @ sk4 @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ sk4 @ '$ki_accessible' ) )
=> ( B @ ( B @ ( B @ or ) @ implies ) @ ( C @ is_a_theorem ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ sk4 @ '$ki_accessible' ) )
=> ( A @ sk5 @ ( A @ sk5 @ ( A @ sk5 @ or ) @ implies ) @ ( B @ is_a_theorem ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_ponens ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: '$ki_world',B: $i,C: '$ki_world',D: $i,E: '$ki_world',F: '$ki_world'] :
@+[G: '$ki_world'] :
~ ( ( G @ ( A @ '$ki_accessible' ) )
=> ( D @ ( G @ is_a_theorem ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: '$ki_world',B: $i,C: '$ki_world',D: $i,E: '$ki_world',F: '$ki_world'] :
@+[G: '$ki_world'] :
~ ( ( G @ ( A @ '$ki_accessible' ) )
=> ( B @ ( D @ implies ) @ ( G @ is_a_theorem ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( G @ is_a_theorem ) ) )
& ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ is_a_theorem ) ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( G @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: '$ki_world'] :
@+[B: $i] :
~ ( ( B @ ( A @ sk11 @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ sk11 @ '$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 @ implies ) @ ( F @ is_a_theorem ) ) )
& ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( B @ ( F @ is_a_theorem ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ sk11 @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( ( ! [E: '$ki_world'] :
( ( E @ ( D @ '$ki_accessible' ) )
=> ( C @ ( A @ sk12 @ implies ) @ ( E @ is_a_theorem ) ) )
& ! [E: '$ki_world'] :
( ( E @ ( D @ '$ki_accessible' ) )
=> ( A @ sk12 @ ( E @ is_a_theorem ) ) ) )
=> ! [E: '$ki_world'] :
( ( E @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ is_a_theorem ) ) ) ) ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: '$ki_world'] :
@+[B: $i] :
~ ( ( B @ ( A @ sk13 @ '$ki_exists_in_world_$i' ) )
=> ! [C: '$ki_world'] :
( ( C @ ( A @ sk13 @ '$ki_accessible' ) )
=> ( ( ! [D: '$ki_world'] :
( ( D @ ( C @ '$ki_accessible' ) )
=> ( B @ ( A @ sk12 @ implies ) @ ( D @ is_a_theorem ) ) )
& ! [D: '$ki_world'] :
( ( D @ ( C @ '$ki_accessible' ) )
=> ( A @ sk12 @ ( D @ is_a_theorem ) ) ) )
=> ! [D: '$ki_world'] :
( ( D @ ( C @ '$ki_accessible' ) )
=> ( B @ ( D @ is_a_theorem ) ) ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ sk13 @ '$ki_accessible' ) )
=> ( ( ! [C: '$ki_world'] :
( ( C @ ( B @ '$ki_accessible' ) )
=> ( A @ sk14 @ ( A @ sk12 @ implies ) @ ( C @ is_a_theorem ) ) )
& ! [C: '$ki_world'] :
( ( C @ ( B @ '$ki_accessible' ) )
=> ( A @ sk12 @ ( C @ is_a_theorem ) ) ) )
=> ! [C: '$ki_world'] :
( ( C @ ( B @ '$ki_accessible' ) )
=> ( A @ sk14 @ ( C @ is_a_theorem ) ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: '$ki_world'] :
@+[B: '$ki_world'] :
~ ( ( B @ ( A @ sk15 @ '$ki_accessible' ) )
=> ( A @ sk14 @ ( B @ is_a_theorem ) ) ) ) ) ).
thf(43,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 @ implies ) @ ( B @ ( F @ implies ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_substitution_2) ).
thf(404,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 @ implies ) @ ( B @ ( F @ implies ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(69,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalence_2_0) ).
thf(622,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(31,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ modus_ponens ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_modus_ponens) ).
thf(306,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ modus_ponens ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(33,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ or_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_2) ).
thf(310,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ or_2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(12,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 @ or ) @ ( B @ ( F @ or ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_substitution_2) ).
thf(158,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 @ or ) @ ( B @ ( F @ or ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
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(74,plain,
! [A: '$ki_world'] :
? [B: $i] : ( B @ ( A @ '$ki_exists_in_world_$i' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(75,plain,
! [A: '$ki_world'] : ( A @ sk2 @ ( A @ '$ki_exists_in_world_$i' ) ),
inference(cnf,[status(esa)],[74]) ).
thf(1,conjecture,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ r2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',verify) ).
thf(2,negated_conjecture,
~ ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ r2 ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(70,plain,
~ ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ r2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(71,plain,
( ~ ( sk1 @ r2 )
& ( sk1 @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(72,plain,
sk1 @ ( '$ki_local_world' @ '$ki_accessible' ),
inference(cnfConj,[status(thm)],[71]) ).
thf(6,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( G @ is_a_theorem ) ) )
& ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ is_a_theorem ) ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( G @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_ponens ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_ponens ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( G @ is_a_theorem ) ) )
& ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ is_a_theorem ) ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( G @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modus_ponens_0) ).
thf(90,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( G @ is_a_theorem ) ) )
& ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ is_a_theorem ) ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( G @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_ponens ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_ponens ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( G @ is_a_theorem ) ) )
& ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ is_a_theorem ) ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( G @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(91,plain,
! [K: '$ki_world',J: '$ki_world',I: '$ki_world',H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ~ ( H @ sk14 @ ( H @ sk16 @ is_a_theorem ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk16 @ ( H @ sk15 @ '$ki_accessible' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk14 @ ( H @ sk12 @ implies ) @ ( J @ is_a_theorem ) )
| ~ ( J @ ( H @ sk15 @ '$ki_accessible' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk12 @ ( I @ is_a_theorem ) )
| ~ ( I @ ( H @ sk15 @ '$ki_accessible' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk15 @ ( H @ sk13 @ '$ki_accessible' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk14 @ ( H @ sk13 @ '$ki_exists_in_world_$i' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk13 @ ( H @ sk11 @ '$ki_accessible' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk12 @ ( H @ sk11 @ '$ki_exists_in_world_$i' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( K @ modus_ponens )
| ~ ( K @ ( H @ '$ki_accessible' ) )
| ( H @ sk11 @ ( H @ '$ki_accessible' ) )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( E @ ( G @ is_a_theorem ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( E @ ( G @ is_a_theorem ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( E @ ( G @ is_a_theorem ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( E @ ( G @ is_a_theorem ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( A @ sk7 )
| ~ ( A @ sk8 @ modus_ponens )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ) ),
inference(cnf,[status(esa)],[90]) ).
thf(97,plain,
! [A: '$ki_world'] :
( ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[91]) ).
thf(964,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ ( '$ki_local_world' @ '$ki_accessible' ) )
!= ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[72,97]) ).
thf(965,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ ( '$ki_local_world' @ '$ki_accessible' ) )
!= ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[964]) ).
thf(966,plain,
( ( sk1 @ sk7 )
| ( sk1 @ sk8 @ ( sk1 @ '$ki_accessible' ) ) ),
inference(pattern_uni,[status(thm)],[965:[bind(A,$thf( sk1 ))]]) ).
thf(1010,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ sk8 @ ( sk1 @ '$ki_accessible' ) )
!= ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) )
| ~ $true
| ( sk1 @ sk7 ) ),
inference(paramod_ordered,[status(thm)],[966,97]) ).
thf(1011,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ sk8 @ ( sk1 @ '$ki_accessible' ) )
!= ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) )
| ( sk1 @ sk7 ) ),
inference(simp,[status(thm)],[1010]) ).
thf(1030,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ sk8 )
!= A )
| ( sk1 != '$ki_local_world' )
| ( A @ sk7 )
| ( A @ sk8 @ ( A @ '$ki_accessible' ) )
| ( sk1 @ sk7 ) ),
inference(simp,[status(thm)],[1011]) ).
thf(1036,plain,
( ( sk1 != '$ki_local_world' )
| ( sk1 @ sk8 @ sk7 )
| ( sk1 @ sk8 @ sk8 @ ( sk1 @ sk8 @ '$ki_accessible' ) )
| ( sk1 @ sk7 ) ),
inference(simp,[status(thm)],[1030]) ).
thf(5,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_or ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_or) ).
thf(88,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_or ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(44,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ implies_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_implies_2) ).
thf(408,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ implies_2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(32,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(308,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)],[32]) ).
thf(8,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_1_0) ).
thf(120,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(48,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 @ implies ) @ ( F @ ( B @ implies ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_substitution_1) ).
thf(440,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 @ implies ) @ ( F @ ( B @ implies ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(61,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ and ) @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ and ) @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_3_0) ).
thf(550,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ and ) @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ and ) @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(11,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( C @ not @ ( E @ not @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_tollens ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_tollens ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( C @ not @ ( E @ not @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modus_tollens_0) ).
thf(142,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( C @ not @ ( E @ not @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_tollens ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ modus_tollens ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( C @ not @ ( E @ not @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(55,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( G @ is_a_theorem ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ ( G @ qmltpeq ) ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ substitution_of_equivalents ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ substitution_of_equivalents ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( G @ is_a_theorem ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ ( G @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',substitution_of_equivalents_0) ).
thf(500,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( G @ is_a_theorem ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ ( G @ qmltpeq ) ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ substitution_of_equivalents ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ substitution_of_equivalents ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( G @ is_a_theorem ) ) )
=> ! [G: '$ki_world'] :
( ( G @ ( F @ '$ki_accessible' ) )
=> ( E @ ( C @ ( G @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(53,axiom,
! [A: '$ki_world'] : ( A @ ( A @ '$ki_accessible' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_reflexive) ).
thf(494,plain,
! [A: '$ki_world'] : ( A @ ( A @ '$ki_accessible' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(495,plain,
! [A: '$ki_world'] : ( A @ ( A @ '$ki_accessible' ) ),
inference(cnf,[status(esa)],[494]) ).
thf(89,plain,
! [A: '$ki_world'] :
( ( A @ op_or )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnf,[status(esa)],[88]) ).
thf(1340,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( A @ ( A @ '$ki_accessible' ) )
!= ( B @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( B @ op_or )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[495,89]) ).
thf(1341,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( A @ ( A @ '$ki_accessible' ) )
!= ( B @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( B @ op_or ) ),
inference(simp,[status(thm)],[1340]) ).
thf(1342,plain,
'$ki_local_world' @ op_or,
inference(pattern_uni,[status(thm)],[1341:[bind(A,$thf( '$ki_local_world' )),bind(B,$thf( '$ki_local_world' ))]]) ).
thf(63,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ equivalence_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_equivalence_2) ).
thf(570,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ equivalence_2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(50,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ not @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ not @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn2_0) ).
thf(460,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ not @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ not @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(967,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( A @ ( A @ '$ki_accessible' ) )
!= ( B @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( B @ sk7 )
| ( B @ sk8 @ ( B @ '$ki_accessible' ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[495,97]) ).
thf(968,plain,
! [B: '$ki_world',A: '$ki_world'] :
( ( ( A @ ( A @ '$ki_accessible' ) )
!= ( B @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( B @ sk7 )
| ( B @ sk8 @ ( B @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[967]) ).
thf(969,plain,
( ( '$ki_local_world' @ sk7 )
| ( '$ki_local_world' @ sk8 @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(pattern_uni,[status(thm)],[968:[bind(A,$thf( '$ki_local_world' )),bind(B,$thf( '$ki_local_world' ))]]) ).
thf(4,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r1_0) ).
thf(76,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(77,plain,
! [F: '$ki_world',E: '$ki_world',D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( F @ r1 )
| ~ ( F @ ( E @ '$ki_accessible' ) )
| ~ ( E @ sk5 @ ( E @ sk5 @ ( E @ sk5 @ or ) @ implies ) @ ( E @ sk6 @ is_a_theorem ) )
| ~ ( E @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( F @ r1 )
| ~ ( F @ ( E @ '$ki_accessible' ) )
| ( E @ sk6 @ ( E @ sk4 @ '$ki_accessible' ) )
| ~ ( E @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( F @ r1 )
| ~ ( F @ ( E @ '$ki_accessible' ) )
| ( E @ sk5 @ ( E @ sk4 @ '$ki_exists_in_world_$i' ) )
| ~ ( E @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( F @ r1 )
| ~ ( F @ ( E @ '$ki_accessible' ) )
| ( E @ sk4 @ ( E @ '$ki_accessible' ) )
| ~ ( E @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk3 @ r1 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
& ( ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ( A @ sk3 @ ( A @ '$ki_accessible' ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(78,plain,
! [D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( C @ ( C @ ( C @ or ) @ implies ) @ ( D @ is_a_theorem ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ( A @ sk3 @ ( A @ '$ki_accessible' ) )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(106,plain,
! [G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( E @ ( G @ is_a_theorem ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(cnfConj,[status(thm)],[91]) ).
thf(52,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ implies_1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_implies_1) ).
thf(492,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ implies_1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(14,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( C @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( C @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalence_3_0) ).
thf(164,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( C @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ equiv ) @ ( C @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
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' ) )
=> ( D @ ( B @ ( H @ qmltpeq ) ) ) )
=> ! [H: '$ki_world'] :
( ( H @ ( G @ '$ki_accessible' ) )
=> ( F @ ( D @ or ) @ ( F @ ( B @ or ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_substitution_1) ).
thf(116,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 @ or ) @ ( F @ ( B @ or ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(47,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ not @ implies ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ not @ implies ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn3_0) ).
thf(428,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ not @ implies ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ ( C @ not @ implies ) @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
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' ) )
=> ! [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 @ not @ ( B @ not @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_substitution_1) ).
thf(206,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 @ not @ ( B @ not @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(34,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_equiv ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',principia_op_equiv) ).
thf(312,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_equiv ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(40,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_and ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',principia_op_and) ).
thf(380,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_and ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(22,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 @ equiv ) @ ( B @ ( F @ equiv ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equiv_substitution_2) ).
thf(220,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 @ equiv ) @ ( B @ ( F @ equiv ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(60,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_2_0) ).
thf(534,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(26,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ and_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_and_2) ).
thf(260,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ and_2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(67,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn1_0) ).
thf(598,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ cn1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(638,plain,
! [N: '$ki_world',M: '$ki_world',L: $i,K: '$ki_world',J: $i,I: '$ki_world',H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( E @ ( G @ is_a_theorem ) )
!= ( J @ ( H @ ( I @ ( J @ ( K @ ( L @ ( M @ sk9 ) ) ) ) ) @ is_a_theorem ) ) )
| ( L @ ( N @ is_a_theorem ) )
| ~ ( N @ ( M @ '$ki_accessible' ) )
| ~ ( L @ ( J @ implies ) @ ( H @ ( I @ ( J @ ( K @ ( L @ ( M @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ $true
| ~ ( M @ ( K @ '$ki_accessible' ) )
| ~ ( L @ ( K @ '$ki_exists_in_world_$i' ) )
| ~ ( K @ ( I @ '$ki_accessible' ) )
| ~ ( J @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( H @ '$ki_accessible' ) )
| ~ ( H @ sk7 )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(paramod_ordered,[status(thm)],[106,106]) ).
thf(639,plain,
! [N: '$ki_world',M: '$ki_world',L: $i,K: '$ki_world',J: $i,I: '$ki_world',H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( E @ ( G @ is_a_theorem ) )
!= ( J @ ( H @ ( I @ ( J @ ( K @ ( L @ ( M @ sk9 ) ) ) ) ) @ is_a_theorem ) ) )
| ( L @ ( N @ is_a_theorem ) )
| ~ ( N @ ( M @ '$ki_accessible' ) )
| ~ ( L @ ( J @ implies ) @ ( H @ ( I @ ( J @ ( K @ ( L @ ( M @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( M @ ( K @ '$ki_accessible' ) )
| ~ ( L @ ( K @ '$ki_exists_in_world_$i' ) )
| ~ ( K @ ( I @ '$ki_accessible' ) )
| ~ ( J @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( H @ '$ki_accessible' ) )
| ~ ( H @ sk7 )
| ~ ( H @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( G @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[638]) ).
thf(640,plain,
! [L: '$ki_world',K: '$ki_world',J: '$ki_world',I: $i,H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( I @ ( G @ is_a_theorem ) )
| ~ ( G @ ( H @ '$ki_accessible' ) )
| ~ ( I @ ( E @ implies ) @ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( H @ ( J @ '$ki_accessible' ) )
| ~ ( I @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( E @ ( K @ '$ki_exists_in_world_$i' ) )
| ~ ( K @ ( L @ '$ki_accessible' ) )
| ~ ( L @ sk7 )
| ~ ( L @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(pattern_uni,[status(thm)],[639:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( T @ ( S @ ( E @ ( Q @ ( P @ ( O @ sk9 ) ) ) ) ) )),bind(H,$thf( T )),bind(I,$thf( S )),bind(J,$thf( E )),bind(K,$thf( Q )),bind(L,$thf( P )),bind(M,$thf( O )),bind(N,$thf( N ))]]) ).
thf(693,plain,
! [L: '$ki_world',K: '$ki_world',J: '$ki_world',I: $i,H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( I @ ( G @ is_a_theorem ) )
| ~ ( G @ ( H @ '$ki_accessible' ) )
| ~ ( I @ ( E @ implies ) @ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( H @ ( J @ '$ki_accessible' ) )
| ~ ( I @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( E @ ( K @ '$ki_exists_in_world_$i' ) )
| ~ ( K @ ( L @ '$ki_accessible' ) )
| ~ ( L @ sk7 )
| ~ ( L @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[640]) ).
thf(62,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_equiv ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( E @ ( C @ implies ) @ and ) @ ( E @ ( C @ equiv ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_equiv_0) ).
thf(566,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_equiv ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( E @ ( C @ implies ) @ and ) @ ( E @ ( C @ equiv ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(56,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_implies_and ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ not @ ( C @ and ) @ not @ ( E @ ( C @ implies ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_implies_and_0) ).
thf(522,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_implies_and ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ not @ ( C @ and ) @ not @ ( E @ ( C @ implies ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(23,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kn2_0) ).
thf(224,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(51,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r2_0) ).
thf(476,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( E @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(57,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_or ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ not @ ( C @ not @ and ) @ not @ ( E @ ( C @ or ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_or_0) ).
thf(526,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_or ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ not @ ( C @ not @ and ) @ not @ ( E @ ( C @ or ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
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: $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(212,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)],[20]) ).
thf(73,plain,
~ ( sk1 @ r2 ),
inference(cnfConj,[status(thm)],[71]) ).
thf(25,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_1_0) ).
thf(244,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ implies ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(29,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ or ) @ ( G @ ( E @ or ) @ ( C @ or ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r4 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r4 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ or ) @ ( G @ ( E @ or ) @ ( C @ or ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r4_0) ).
thf(266,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ or ) @ ( G @ ( E @ or ) @ ( C @ or ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r4 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r4 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ or ) @ ( G @ ( E @ or ) @ ( C @ or ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(58,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_equiv ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_equiv) ).
thf(530,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_equiv ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(46,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ implies ) @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ implies ) @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_2_0) ).
thf(412,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ implies ) @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ implies ) @ ( C @ implies ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(68,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 @ and ) @ ( B @ ( F @ and ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_substitution_2) ).
thf(618,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 @ and ) @ ( B @ ( F @ and ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(28,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ substitution_of_equivalents ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',substitution_of_equivalents_1) ).
thf(264,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ substitution_of_equivalents ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(15,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_3_0) ).
thf(180,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ implies_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(49,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalence_1_0) ).
thf(444,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ equivalence_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ implies ) @ ( E @ ( C @ equiv ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(42,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ equivalence_1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_equivalence_1) ).
thf(402,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ equivalence_1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(30,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ and ) @ not @ ( G @ ( E @ and ) @ not @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ and ) @ not @ ( G @ ( E @ and ) @ not @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kn3_0) ).
thf(286,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ and ) @ not @ ( G @ ( E @ and ) @ not @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( C @ ( G @ and ) @ not @ ( G @ ( E @ and ) @ not @ implies ) @ ( E @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(17,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ or_1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_1) ).
thf(204,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ or_1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(41,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r5 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r5 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r5_0) ).
thf(382,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r5 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r5 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( C @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(64,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( G @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( G @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_3_0) ).
thf(572,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( G @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ! [G: $i] :
( ( G @ ( F @ '$ki_exists_in_world_$i' ) )
=> ! [H: '$ki_world'] :
( ( H @ ( F @ '$ki_accessible' ) )
=> ( G @ ( E @ ( C @ or ) @ implies ) @ ( G @ ( E @ implies ) @ implies ) @ ( G @ ( C @ implies ) @ implies ) @ ( H @ is_a_theorem ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(725,plain,
! [X: '$ki_world',W: '$ki_world',V: '$ki_world',U: $i,T: '$ki_world',S: '$ki_world',R: '$ki_world',Q: $i,P: '$ki_world',O: $i,N: '$ki_world',M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: $i,H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( I @ ( G @ is_a_theorem ) )
!= ( O @ ( M @ ( N @ ( O @ ( P @ ( Q @ ( R @ sk9 ) ) ) ) ) @ is_a_theorem ) ) )
| ( U @ ( S @ is_a_theorem ) )
| ~ ( S @ ( T @ '$ki_accessible' ) )
| ~ ( U @ ( Q @ implies ) @ ( X @ ( W @ ( Q @ ( V @ ( U @ ( T @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( T @ ( V @ '$ki_accessible' ) )
| ~ ( U @ ( V @ '$ki_exists_in_world_$i' ) )
| ~ ( V @ ( W @ '$ki_accessible' ) )
| ~ ( Q @ ( W @ '$ki_exists_in_world_$i' ) )
| ~ ( W @ ( X @ '$ki_accessible' ) )
| ~ ( X @ sk7 )
| ~ ( X @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( X @ ( W @ ( Q @ ( V @ ( U @ ( T @ sk9 ) ) ) ) ) @ ( R @ '$ki_accessible' ) )
| ~ ( Q @ ( O @ implies ) @ ( M @ ( N @ ( O @ ( P @ ( Q @ ( R @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ $true
| ~ ( R @ ( P @ '$ki_accessible' ) )
| ~ ( Q @ ( P @ '$ki_exists_in_world_$i' ) )
| ~ ( P @ ( N @ '$ki_accessible' ) )
| ~ ( O @ ( N @ '$ki_exists_in_world_$i' ) )
| ~ ( N @ ( M @ '$ki_accessible' ) )
| ~ ( M @ sk7 )
| ~ ( M @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( G @ ( H @ '$ki_accessible' ) )
| ~ ( I @ ( E @ implies ) @ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( H @ ( J @ '$ki_accessible' ) )
| ~ ( I @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( E @ ( K @ '$ki_exists_in_world_$i' ) )
| ~ ( K @ ( L @ '$ki_accessible' ) )
| ~ ( L @ sk7 )
| ~ ( L @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(paramod_ordered,[status(thm)],[693,693]) ).
thf(726,plain,
! [X: '$ki_world',W: '$ki_world',V: '$ki_world',U: $i,T: '$ki_world',S: '$ki_world',R: '$ki_world',Q: $i,P: '$ki_world',O: $i,N: '$ki_world',M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: $i,H: '$ki_world',G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( I @ ( G @ is_a_theorem ) )
!= ( O @ ( M @ ( N @ ( O @ ( P @ ( Q @ ( R @ sk9 ) ) ) ) ) @ is_a_theorem ) ) )
| ( U @ ( S @ is_a_theorem ) )
| ~ ( S @ ( T @ '$ki_accessible' ) )
| ~ ( U @ ( Q @ implies ) @ ( X @ ( W @ ( Q @ ( V @ ( U @ ( T @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( T @ ( V @ '$ki_accessible' ) )
| ~ ( U @ ( V @ '$ki_exists_in_world_$i' ) )
| ~ ( V @ ( W @ '$ki_accessible' ) )
| ~ ( Q @ ( W @ '$ki_exists_in_world_$i' ) )
| ~ ( W @ ( X @ '$ki_accessible' ) )
| ~ ( X @ sk7 )
| ~ ( X @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( X @ ( W @ ( Q @ ( V @ ( U @ ( T @ sk9 ) ) ) ) ) @ ( R @ '$ki_accessible' ) )
| ~ ( Q @ ( O @ implies ) @ ( M @ ( N @ ( O @ ( P @ ( Q @ ( R @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( R @ ( P @ '$ki_accessible' ) )
| ~ ( Q @ ( P @ '$ki_exists_in_world_$i' ) )
| ~ ( P @ ( N @ '$ki_accessible' ) )
| ~ ( O @ ( N @ '$ki_exists_in_world_$i' ) )
| ~ ( N @ ( M @ '$ki_accessible' ) )
| ~ ( M @ sk7 )
| ~ ( M @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( G @ ( H @ '$ki_accessible' ) )
| ~ ( I @ ( E @ implies ) @ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( H @ ( J @ '$ki_accessible' ) )
| ~ ( I @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( E @ ( K @ '$ki_exists_in_world_$i' ) )
| ~ ( K @ ( L @ '$ki_accessible' ) )
| ~ ( L @ sk7 )
| ~ ( L @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( L @ ( K @ ( E @ ( J @ ( I @ ( H @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[725]) ).
thf(727,plain,
! [V: '$ki_world',U: '$ki_world',T: '$ki_world',S: $i,R: '$ki_world',Q: '$ki_world',P: '$ki_world',O: '$ki_world',N: $i,M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: $i,G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( N @ ( L @ is_a_theorem ) )
| ~ ( L @ ( M @ '$ki_accessible' ) )
| ~ ( N @ ( S @ implies ) @ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( M @ ( O @ '$ki_accessible' ) )
| ~ ( N @ ( O @ '$ki_exists_in_world_$i' ) )
| ~ ( O @ ( P @ '$ki_accessible' ) )
| ~ ( S @ ( P @ '$ki_exists_in_world_$i' ) )
| ~ ( P @ ( Q @ '$ki_accessible' ) )
| ~ ( Q @ sk7 )
| ~ ( Q @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk9 ) ) ) ) ) @ ( R @ '$ki_accessible' ) )
| ~ ( S @ ( H @ implies ) @ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( R @ ( T @ '$ki_accessible' ) )
| ~ ( S @ ( T @ '$ki_exists_in_world_$i' ) )
| ~ ( T @ ( U @ '$ki_accessible' ) )
| ~ ( H @ ( U @ '$ki_exists_in_world_$i' ) )
| ~ ( U @ ( V @ '$ki_accessible' ) )
| ~ ( V @ sk7 )
| ~ ( V @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk9 ) ) ) ) ) @ ( G @ '$ki_accessible' ) )
| ~ ( H @ ( E @ implies ) @ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( G @ ( I @ '$ki_accessible' ) )
| ~ ( H @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( J @ '$ki_accessible' ) )
| ~ ( E @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( K @ sk7 )
| ~ ( K @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(pattern_uni,[status(thm)],[726:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( ZD @ ( ZC @ ( I @ ( ZA @ ( Z @ ( Y @ sk9 ) ) ) ) ) )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( K )),bind(L,$thf( L )),bind(M,$thf( ZD )),bind(N,$thf( ZC )),bind(O,$thf( I )),bind(P,$thf( ZA )),bind(Q,$thf( Z )),bind(R,$thf( Y )),bind(S,$thf( S )),bind(T,$thf( T )),bind(U,$thf( U )),bind(V,$thf( V )),bind(W,$thf( W )),bind(X,$thf( X ))]]) ).
thf(900,plain,
! [V: '$ki_world',U: '$ki_world',T: '$ki_world',S: $i,R: '$ki_world',Q: '$ki_world',P: '$ki_world',O: '$ki_world',N: $i,M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: $i,G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( N @ ( L @ is_a_theorem ) )
| ~ ( L @ ( M @ '$ki_accessible' ) )
| ~ ( N @ ( S @ implies ) @ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( M @ ( O @ '$ki_accessible' ) )
| ~ ( N @ ( O @ '$ki_exists_in_world_$i' ) )
| ~ ( O @ ( P @ '$ki_accessible' ) )
| ~ ( S @ ( P @ '$ki_exists_in_world_$i' ) )
| ~ ( P @ ( Q @ '$ki_accessible' ) )
| ~ ( Q @ sk7 )
| ~ ( Q @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk9 ) ) ) ) ) @ ( R @ '$ki_accessible' ) )
| ~ ( S @ ( H @ implies ) @ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( R @ ( T @ '$ki_accessible' ) )
| ~ ( S @ ( T @ '$ki_exists_in_world_$i' ) )
| ~ ( T @ ( U @ '$ki_accessible' ) )
| ~ ( H @ ( U @ '$ki_exists_in_world_$i' ) )
| ~ ( U @ ( V @ '$ki_accessible' ) )
| ~ ( V @ sk7 )
| ~ ( V @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk9 ) ) ) ) ) @ ( G @ '$ki_accessible' ) )
| ~ ( H @ ( E @ implies ) @ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( G @ ( I @ '$ki_accessible' ) )
| ~ ( H @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( J @ '$ki_accessible' ) )
| ~ ( E @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( K @ sk7 )
| ~ ( K @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[727]) ).
thf(1337,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ ( '$ki_local_world' @ '$ki_accessible' ) )
!= ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( A @ op_or )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[72,89]) ).
thf(1338,plain,
! [A: '$ki_world'] :
( ( ( sk1 @ ( '$ki_local_world' @ '$ki_accessible' ) )
!= ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) )
| ( A @ op_or ) ),
inference(simp,[status(thm)],[1337]) ).
thf(1339,plain,
sk1 @ op_or,
inference(pattern_uni,[status(thm)],[1338:[bind(A,$thf( sk1 ))]]) ).
thf(10,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_implies_or ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',principia_op_implies_or) ).
thf(140,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_implies_or ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(24,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_implies_or ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ not @ or ) @ ( E @ ( C @ implies ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_implies_or_0) ).
thf(240,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_implies_or ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ not @ or ) @ ( E @ ( C @ implies ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(36,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ and ) @ ( C @ implies ) @ ( D @ is_a_theorem ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ and ) @ ( C @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kn1_0) ).
thf(330,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ and ) @ ( C @ implies ) @ ( D @ is_a_theorem ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ kn1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ( C @ ( C @ and ) @ ( C @ implies ) @ ( D @ is_a_theorem ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(13,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ equivalence_3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_equivalence_3) ).
thf(162,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ equivalence_3 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(37,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_2_0) ).
thf(342,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_2 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ and_2 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( E @ ( C @ and ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(35,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_1_0) ).
thf(314,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_1 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ or_1 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ ( C @ or ) @ ( C @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(21,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ and_3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_and_3) ).
thf(218,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ and_3 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(1488,plain,
! [ZR: '$ki_world',ZQ: '$ki_world',ZP: '$ki_world',ZO: $i,ZN: '$ki_world',ZM: '$ki_world',ZL: '$ki_world',ZK: '$ki_world',ZJ: $i,ZI: '$ki_world',ZH: '$ki_world',ZG: '$ki_world',ZF: '$ki_world',ZE: '$ki_world',ZD: $i,ZC: '$ki_world',ZB: '$ki_world',ZA: $i,Z: '$ki_world',Y: $i,X: '$ki_world',W: '$ki_world',V: '$ki_world',U: '$ki_world',T: '$ki_world',S: $i,R: '$ki_world',Q: '$ki_world',P: '$ki_world',O: '$ki_world',N: $i,M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: $i,G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( N @ ( L @ is_a_theorem ) )
!= ( Y @ ( W @ ( X @ ( Y @ ( Z @ ( ZA @ ( ZB @ sk9 ) ) ) ) ) @ is_a_theorem ) ) )
| ( ZJ @ ( ZH @ is_a_theorem ) )
| ~ ( ZH @ ( ZI @ '$ki_accessible' ) )
| ~ ( ZJ @ ( ZO @ implies ) @ ( ZM @ ( ZL @ ( ZO @ ( ZK @ ( ZJ @ ( ZI @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZI @ ( ZK @ '$ki_accessible' ) )
| ~ ( ZJ @ ( ZK @ '$ki_exists_in_world_$i' ) )
| ~ ( ZK @ ( ZL @ '$ki_accessible' ) )
| ~ ( ZO @ ( ZL @ '$ki_exists_in_world_$i' ) )
| ~ ( ZL @ ( ZM @ '$ki_accessible' ) )
| ~ ( ZM @ sk7 )
| ~ ( ZM @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZM @ ( ZL @ ( ZO @ ( ZK @ ( ZJ @ ( ZI @ sk9 ) ) ) ) ) @ ( ZN @ '$ki_accessible' ) )
| ~ ( ZO @ ( ZD @ implies ) @ ( ZR @ ( ZQ @ ( ZD @ ( ZP @ ( ZO @ ( ZN @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZN @ ( ZP @ '$ki_accessible' ) )
| ~ ( ZO @ ( ZP @ '$ki_exists_in_world_$i' ) )
| ~ ( ZP @ ( ZQ @ '$ki_accessible' ) )
| ~ ( ZD @ ( ZQ @ '$ki_exists_in_world_$i' ) )
| ~ ( ZQ @ ( ZR @ '$ki_accessible' ) )
| ~ ( ZR @ sk7 )
| ~ ( ZR @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZR @ ( ZQ @ ( ZD @ ( ZP @ ( ZO @ ( ZN @ sk9 ) ) ) ) ) @ ( ZC @ '$ki_accessible' ) )
| ~ ( ZD @ ( ZA @ implies ) @ ( ZG @ ( ZF @ ( ZA @ ( ZE @ ( ZD @ ( ZC @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZC @ ( ZE @ '$ki_accessible' ) )
| ~ ( ZD @ ( ZE @ '$ki_exists_in_world_$i' ) )
| ~ ( ZE @ ( ZF @ '$ki_accessible' ) )
| ~ ( ZA @ ( ZF @ '$ki_exists_in_world_$i' ) )
| ~ ( ZF @ ( ZG @ '$ki_accessible' ) )
| ~ ( ZG @ sk7 )
| ~ ( ZG @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZG @ ( ZF @ ( ZA @ ( ZE @ ( ZD @ ( ZC @ sk9 ) ) ) ) ) @ ( ZB @ '$ki_accessible' ) )
| ~ ( ZA @ ( Y @ implies ) @ ( W @ ( X @ ( Y @ ( Z @ ( ZA @ ( ZB @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ $true
| ~ ( ZB @ ( Z @ '$ki_accessible' ) )
| ~ ( ZA @ ( Z @ '$ki_exists_in_world_$i' ) )
| ~ ( Z @ ( X @ '$ki_accessible' ) )
| ~ ( Y @ ( X @ '$ki_exists_in_world_$i' ) )
| ~ ( X @ ( W @ '$ki_accessible' ) )
| ~ ( W @ sk7 )
| ~ ( W @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( L @ ( M @ '$ki_accessible' ) )
| ~ ( N @ ( S @ implies ) @ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( M @ ( O @ '$ki_accessible' ) )
| ~ ( N @ ( O @ '$ki_exists_in_world_$i' ) )
| ~ ( O @ ( P @ '$ki_accessible' ) )
| ~ ( S @ ( P @ '$ki_exists_in_world_$i' ) )
| ~ ( P @ ( Q @ '$ki_accessible' ) )
| ~ ( Q @ sk7 )
| ~ ( Q @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk9 ) ) ) ) ) @ ( R @ '$ki_accessible' ) )
| ~ ( S @ ( H @ implies ) @ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( R @ ( T @ '$ki_accessible' ) )
| ~ ( S @ ( T @ '$ki_exists_in_world_$i' ) )
| ~ ( T @ ( U @ '$ki_accessible' ) )
| ~ ( H @ ( U @ '$ki_exists_in_world_$i' ) )
| ~ ( U @ ( V @ '$ki_accessible' ) )
| ~ ( V @ sk7 )
| ~ ( V @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk9 ) ) ) ) ) @ ( G @ '$ki_accessible' ) )
| ~ ( H @ ( E @ implies ) @ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( G @ ( I @ '$ki_accessible' ) )
| ~ ( H @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( J @ '$ki_accessible' ) )
| ~ ( E @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( K @ sk7 )
| ~ ( K @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(paramod_ordered,[status(thm)],[900,900]) ).
thf(1489,plain,
! [ZR: '$ki_world',ZQ: '$ki_world',ZP: '$ki_world',ZO: $i,ZN: '$ki_world',ZM: '$ki_world',ZL: '$ki_world',ZK: '$ki_world',ZJ: $i,ZI: '$ki_world',ZH: '$ki_world',ZG: '$ki_world',ZF: '$ki_world',ZE: '$ki_world',ZD: $i,ZC: '$ki_world',ZB: '$ki_world',ZA: $i,Z: '$ki_world',Y: $i,X: '$ki_world',W: '$ki_world',V: '$ki_world',U: '$ki_world',T: '$ki_world',S: $i,R: '$ki_world',Q: '$ki_world',P: '$ki_world',O: '$ki_world',N: $i,M: '$ki_world',L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: $i,G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ( N @ ( L @ is_a_theorem ) )
!= ( Y @ ( W @ ( X @ ( Y @ ( Z @ ( ZA @ ( ZB @ sk9 ) ) ) ) ) @ is_a_theorem ) ) )
| ( ZJ @ ( ZH @ is_a_theorem ) )
| ~ ( ZH @ ( ZI @ '$ki_accessible' ) )
| ~ ( ZJ @ ( ZO @ implies ) @ ( ZM @ ( ZL @ ( ZO @ ( ZK @ ( ZJ @ ( ZI @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZI @ ( ZK @ '$ki_accessible' ) )
| ~ ( ZJ @ ( ZK @ '$ki_exists_in_world_$i' ) )
| ~ ( ZK @ ( ZL @ '$ki_accessible' ) )
| ~ ( ZO @ ( ZL @ '$ki_exists_in_world_$i' ) )
| ~ ( ZL @ ( ZM @ '$ki_accessible' ) )
| ~ ( ZM @ sk7 )
| ~ ( ZM @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZM @ ( ZL @ ( ZO @ ( ZK @ ( ZJ @ ( ZI @ sk9 ) ) ) ) ) @ ( ZN @ '$ki_accessible' ) )
| ~ ( ZO @ ( ZD @ implies ) @ ( ZR @ ( ZQ @ ( ZD @ ( ZP @ ( ZO @ ( ZN @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZN @ ( ZP @ '$ki_accessible' ) )
| ~ ( ZO @ ( ZP @ '$ki_exists_in_world_$i' ) )
| ~ ( ZP @ ( ZQ @ '$ki_accessible' ) )
| ~ ( ZD @ ( ZQ @ '$ki_exists_in_world_$i' ) )
| ~ ( ZQ @ ( ZR @ '$ki_accessible' ) )
| ~ ( ZR @ sk7 )
| ~ ( ZR @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZR @ ( ZQ @ ( ZD @ ( ZP @ ( ZO @ ( ZN @ sk9 ) ) ) ) ) @ ( ZC @ '$ki_accessible' ) )
| ~ ( ZD @ ( ZA @ implies ) @ ( ZG @ ( ZF @ ( ZA @ ( ZE @ ( ZD @ ( ZC @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZC @ ( ZE @ '$ki_accessible' ) )
| ~ ( ZD @ ( ZE @ '$ki_exists_in_world_$i' ) )
| ~ ( ZE @ ( ZF @ '$ki_accessible' ) )
| ~ ( ZA @ ( ZF @ '$ki_exists_in_world_$i' ) )
| ~ ( ZF @ ( ZG @ '$ki_accessible' ) )
| ~ ( ZG @ sk7 )
| ~ ( ZG @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZG @ ( ZF @ ( ZA @ ( ZE @ ( ZD @ ( ZC @ sk9 ) ) ) ) ) @ ( ZB @ '$ki_accessible' ) )
| ~ ( ZA @ ( Y @ implies ) @ ( W @ ( X @ ( Y @ ( Z @ ( ZA @ ( ZB @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZB @ ( Z @ '$ki_accessible' ) )
| ~ ( ZA @ ( Z @ '$ki_exists_in_world_$i' ) )
| ~ ( Z @ ( X @ '$ki_accessible' ) )
| ~ ( Y @ ( X @ '$ki_exists_in_world_$i' ) )
| ~ ( X @ ( W @ '$ki_accessible' ) )
| ~ ( W @ sk7 )
| ~ ( W @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( L @ ( M @ '$ki_accessible' ) )
| ~ ( N @ ( S @ implies ) @ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( M @ ( O @ '$ki_accessible' ) )
| ~ ( N @ ( O @ '$ki_exists_in_world_$i' ) )
| ~ ( O @ ( P @ '$ki_accessible' ) )
| ~ ( S @ ( P @ '$ki_exists_in_world_$i' ) )
| ~ ( P @ ( Q @ '$ki_accessible' ) )
| ~ ( Q @ sk7 )
| ~ ( Q @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( Q @ ( P @ ( S @ ( O @ ( N @ ( M @ sk9 ) ) ) ) ) @ ( R @ '$ki_accessible' ) )
| ~ ( S @ ( H @ implies ) @ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( R @ ( T @ '$ki_accessible' ) )
| ~ ( S @ ( T @ '$ki_exists_in_world_$i' ) )
| ~ ( T @ ( U @ '$ki_accessible' ) )
| ~ ( H @ ( U @ '$ki_exists_in_world_$i' ) )
| ~ ( U @ ( V @ '$ki_accessible' ) )
| ~ ( V @ sk7 )
| ~ ( V @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( V @ ( U @ ( H @ ( T @ ( S @ ( R @ sk9 ) ) ) ) ) @ ( G @ '$ki_accessible' ) )
| ~ ( H @ ( E @ implies ) @ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( G @ ( I @ '$ki_accessible' ) )
| ~ ( H @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( J @ '$ki_accessible' ) )
| ~ ( E @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( K @ sk7 )
| ~ ( K @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[1488]) ).
thf(1490,plain,
! [ZP: '$ki_world',ZO: '$ki_world',ZN: '$ki_world',ZM: $i,ZL: '$ki_world',ZK: '$ki_world',ZJ: '$ki_world',ZI: '$ki_world',ZH: $i,ZG: '$ki_world',ZF: '$ki_world',ZE: '$ki_world',ZD: '$ki_world',ZC: $i,ZB: '$ki_world',ZA: '$ki_world',Z: '$ki_world',Y: '$ki_world',X: '$ki_world',W: $i,V: '$ki_world',U: '$ki_world',T: '$ki_world',S: '$ki_world',R: $i,Q: '$ki_world',P: '$ki_world',O: '$ki_world',N: '$ki_world',M: $i,L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: $i,G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ZC @ ( ZA @ is_a_theorem ) )
| ~ ( ZA @ ( ZB @ '$ki_accessible' ) )
| ~ ( ZC @ ( ZH @ implies ) @ ( ZF @ ( ZE @ ( ZH @ ( ZD @ ( ZC @ ( ZB @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZB @ ( ZD @ '$ki_accessible' ) )
| ~ ( ZC @ ( ZD @ '$ki_exists_in_world_$i' ) )
| ~ ( ZD @ ( ZE @ '$ki_accessible' ) )
| ~ ( ZH @ ( ZE @ '$ki_exists_in_world_$i' ) )
| ~ ( ZE @ ( ZF @ '$ki_accessible' ) )
| ~ ( ZF @ sk7 )
| ~ ( ZF @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZF @ ( ZE @ ( ZH @ ( ZD @ ( ZC @ ( ZB @ sk9 ) ) ) ) ) @ ( ZG @ '$ki_accessible' ) )
| ~ ( ZH @ ( W @ implies ) @ ( ZK @ ( ZJ @ ( W @ ( ZI @ ( ZH @ ( ZG @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZG @ ( ZI @ '$ki_accessible' ) )
| ~ ( ZH @ ( ZI @ '$ki_exists_in_world_$i' ) )
| ~ ( ZI @ ( ZJ @ '$ki_accessible' ) )
| ~ ( W @ ( ZJ @ '$ki_exists_in_world_$i' ) )
| ~ ( ZJ @ ( ZK @ '$ki_accessible' ) )
| ~ ( ZK @ sk7 )
| ~ ( ZK @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZK @ ( ZJ @ ( W @ ( ZI @ ( ZH @ ( ZG @ sk9 ) ) ) ) ) @ ( V @ '$ki_accessible' ) )
| ~ ( W @ ( ZM @ implies ) @ ( Z @ ( Y @ ( ZM @ ( X @ ( W @ ( V @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( V @ ( X @ '$ki_accessible' ) )
| ~ ( W @ ( X @ '$ki_exists_in_world_$i' ) )
| ~ ( X @ ( Y @ '$ki_accessible' ) )
| ~ ( ZM @ ( Y @ '$ki_exists_in_world_$i' ) )
| ~ ( Y @ ( Z @ '$ki_accessible' ) )
| ~ ( Z @ sk7 )
| ~ ( Z @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( Z @ ( Y @ ( ZM @ ( X @ ( W @ ( V @ sk9 ) ) ) ) ) @ ( ZL @ '$ki_accessible' ) )
| ~ ( ZM @ ( M @ implies ) @ ( ZP @ ( ZO @ ( M @ ( ZN @ ( ZM @ ( ZL @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZL @ ( ZN @ '$ki_accessible' ) )
| ~ ( ZM @ ( ZN @ '$ki_exists_in_world_$i' ) )
| ~ ( ZN @ ( ZO @ '$ki_accessible' ) )
| ~ ( M @ ( ZO @ '$ki_exists_in_world_$i' ) )
| ~ ( ZO @ ( ZP @ '$ki_accessible' ) )
| ~ ( ZP @ sk7 )
| ~ ( ZP @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZP @ ( ZO @ ( M @ ( ZN @ ( ZM @ ( ZL @ sk9 ) ) ) ) ) @ ( L @ '$ki_accessible' ) )
| ~ ( M @ ( R @ implies ) @ ( P @ ( O @ ( R @ ( N @ ( M @ ( L @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( L @ ( N @ '$ki_accessible' ) )
| ~ ( M @ ( N @ '$ki_exists_in_world_$i' ) )
| ~ ( N @ ( O @ '$ki_accessible' ) )
| ~ ( R @ ( O @ '$ki_exists_in_world_$i' ) )
| ~ ( O @ ( P @ '$ki_accessible' ) )
| ~ ( P @ sk7 )
| ~ ( P @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( P @ ( O @ ( R @ ( N @ ( M @ ( L @ sk9 ) ) ) ) ) @ ( Q @ '$ki_accessible' ) )
| ~ ( R @ ( H @ implies ) @ ( U @ ( T @ ( H @ ( S @ ( R @ ( Q @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( Q @ ( S @ '$ki_accessible' ) )
| ~ ( R @ ( S @ '$ki_exists_in_world_$i' ) )
| ~ ( S @ ( T @ '$ki_accessible' ) )
| ~ ( H @ ( T @ '$ki_exists_in_world_$i' ) )
| ~ ( T @ ( U @ '$ki_accessible' ) )
| ~ ( U @ sk7 )
| ~ ( U @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( U @ ( T @ ( H @ ( S @ ( R @ ( Q @ sk9 ) ) ) ) ) @ ( G @ '$ki_accessible' ) )
| ~ ( H @ ( E @ implies ) @ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( G @ ( I @ '$ki_accessible' ) )
| ~ ( H @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( J @ '$ki_accessible' ) )
| ~ ( E @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( K @ sk7 )
| ~ ( K @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(pattern_uni,[status(thm)],[1489:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( K )),bind(L,$thf( ZX @ ( ZW @ ( N @ ( ZU @ ( ZT @ ( ZS @ sk9 ) ) ) ) ) )),bind(M,$thf( M )),bind(N,$thf( N )),bind(O,$thf( O )),bind(P,$thf( P )),bind(Q,$thf( Q )),bind(R,$thf( R )),bind(S,$thf( S )),bind(T,$thf( T )),bind(U,$thf( U )),bind(V,$thf( V )),bind(W,$thf( ZX )),bind(X,$thf( ZW )),bind(Y,$thf( N )),bind(Z,$thf( ZU )),bind(ZA,$thf( ZT )),bind(ZB,$thf( ZS )),bind(ZC,$thf( ZC )),bind(ZD,$thf( ZD )),bind(ZE,$thf( ZE )),bind(ZF,$thf( ZF )),bind(ZG,$thf( ZG )),bind(ZH,$thf( ZH )),bind(ZI,$thf( ZI )),bind(ZJ,$thf( ZJ )),bind(ZK,$thf( ZK )),bind(ZL,$thf( ZL )),bind(ZM,$thf( ZM )),bind(ZN,$thf( ZN )),bind(ZO,$thf( ZO )),bind(ZP,$thf( ZP )),bind(ZQ,$thf( ZQ )),bind(ZR,$thf( ZR ))]]) ).
thf(2302,plain,
! [ZP: '$ki_world',ZO: '$ki_world',ZN: '$ki_world',ZM: $i,ZL: '$ki_world',ZK: '$ki_world',ZJ: '$ki_world',ZI: '$ki_world',ZH: $i,ZG: '$ki_world',ZF: '$ki_world',ZE: '$ki_world',ZD: '$ki_world',ZC: $i,ZB: '$ki_world',ZA: '$ki_world',Z: '$ki_world',Y: '$ki_world',X: '$ki_world',W: $i,V: '$ki_world',U: '$ki_world',T: '$ki_world',S: '$ki_world',R: $i,Q: '$ki_world',P: '$ki_world',O: '$ki_world',N: '$ki_world',M: $i,L: '$ki_world',K: '$ki_world',J: '$ki_world',I: '$ki_world',H: $i,G: '$ki_world',F: '$ki_world',E: $i,D: '$ki_world',C: $i,B: '$ki_world',A: '$ki_world'] :
( ( ZC @ ( ZA @ is_a_theorem ) )
| ~ ( ZA @ ( ZB @ '$ki_accessible' ) )
| ~ ( ZC @ ( ZH @ implies ) @ ( ZF @ ( ZE @ ( ZH @ ( ZD @ ( ZC @ ( ZB @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZB @ ( ZD @ '$ki_accessible' ) )
| ~ ( ZC @ ( ZD @ '$ki_exists_in_world_$i' ) )
| ~ ( ZD @ ( ZE @ '$ki_accessible' ) )
| ~ ( ZH @ ( ZE @ '$ki_exists_in_world_$i' ) )
| ~ ( ZE @ ( ZF @ '$ki_accessible' ) )
| ~ ( ZF @ sk7 )
| ~ ( ZF @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZF @ ( ZE @ ( ZH @ ( ZD @ ( ZC @ ( ZB @ sk9 ) ) ) ) ) @ ( ZG @ '$ki_accessible' ) )
| ~ ( ZH @ ( W @ implies ) @ ( ZK @ ( ZJ @ ( W @ ( ZI @ ( ZH @ ( ZG @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZG @ ( ZI @ '$ki_accessible' ) )
| ~ ( ZH @ ( ZI @ '$ki_exists_in_world_$i' ) )
| ~ ( ZI @ ( ZJ @ '$ki_accessible' ) )
| ~ ( W @ ( ZJ @ '$ki_exists_in_world_$i' ) )
| ~ ( ZJ @ ( ZK @ '$ki_accessible' ) )
| ~ ( ZK @ sk7 )
| ~ ( ZK @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZK @ ( ZJ @ ( W @ ( ZI @ ( ZH @ ( ZG @ sk9 ) ) ) ) ) @ ( V @ '$ki_accessible' ) )
| ~ ( W @ ( ZM @ implies ) @ ( Z @ ( Y @ ( ZM @ ( X @ ( W @ ( V @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( V @ ( X @ '$ki_accessible' ) )
| ~ ( W @ ( X @ '$ki_exists_in_world_$i' ) )
| ~ ( X @ ( Y @ '$ki_accessible' ) )
| ~ ( ZM @ ( Y @ '$ki_exists_in_world_$i' ) )
| ~ ( Y @ ( Z @ '$ki_accessible' ) )
| ~ ( Z @ sk7 )
| ~ ( Z @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( Z @ ( Y @ ( ZM @ ( X @ ( W @ ( V @ sk9 ) ) ) ) ) @ ( ZL @ '$ki_accessible' ) )
| ~ ( ZM @ ( M @ implies ) @ ( ZP @ ( ZO @ ( M @ ( ZN @ ( ZM @ ( ZL @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( ZL @ ( ZN @ '$ki_accessible' ) )
| ~ ( ZM @ ( ZN @ '$ki_exists_in_world_$i' ) )
| ~ ( ZN @ ( ZO @ '$ki_accessible' ) )
| ~ ( M @ ( ZO @ '$ki_exists_in_world_$i' ) )
| ~ ( ZO @ ( ZP @ '$ki_accessible' ) )
| ~ ( ZP @ sk7 )
| ~ ( ZP @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( ZP @ ( ZO @ ( M @ ( ZN @ ( ZM @ ( ZL @ sk9 ) ) ) ) ) @ ( L @ '$ki_accessible' ) )
| ~ ( M @ ( R @ implies ) @ ( P @ ( O @ ( R @ ( N @ ( M @ ( L @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( L @ ( N @ '$ki_accessible' ) )
| ~ ( M @ ( N @ '$ki_exists_in_world_$i' ) )
| ~ ( N @ ( O @ '$ki_accessible' ) )
| ~ ( R @ ( O @ '$ki_exists_in_world_$i' ) )
| ~ ( O @ ( P @ '$ki_accessible' ) )
| ~ ( P @ sk7 )
| ~ ( P @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( P @ ( O @ ( R @ ( N @ ( M @ ( L @ sk9 ) ) ) ) ) @ ( Q @ '$ki_accessible' ) )
| ~ ( R @ ( H @ implies ) @ ( U @ ( T @ ( H @ ( S @ ( R @ ( Q @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( Q @ ( S @ '$ki_accessible' ) )
| ~ ( R @ ( S @ '$ki_exists_in_world_$i' ) )
| ~ ( S @ ( T @ '$ki_accessible' ) )
| ~ ( H @ ( T @ '$ki_exists_in_world_$i' ) )
| ~ ( T @ ( U @ '$ki_accessible' ) )
| ~ ( U @ sk7 )
| ~ ( U @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( U @ ( T @ ( H @ ( S @ ( R @ ( Q @ sk9 ) ) ) ) ) @ ( G @ '$ki_accessible' ) )
| ~ ( H @ ( E @ implies ) @ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( G @ ( I @ '$ki_accessible' ) )
| ~ ( H @ ( I @ '$ki_exists_in_world_$i' ) )
| ~ ( I @ ( J @ '$ki_accessible' ) )
| ~ ( E @ ( J @ '$ki_exists_in_world_$i' ) )
| ~ ( J @ ( K @ '$ki_accessible' ) )
| ~ ( K @ sk7 )
| ~ ( K @ ( '$ki_local_world' @ '$ki_accessible' ) )
| ~ ( K @ ( J @ ( E @ ( I @ ( H @ ( G @ sk9 ) ) ) ) ) @ ( F @ '$ki_accessible' ) )
| ~ ( E @ ( C @ implies ) @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk10 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk9 ) ) ) ) ) @ is_a_theorem ) )
| ~ ( F @ ( D @ '$ki_accessible' ) )
| ~ ( E @ ( D @ '$ki_exists_in_world_$i' ) )
| ~ ( D @ ( B @ '$ki_accessible' ) )
| ~ ( C @ ( B @ '$ki_exists_in_world_$i' ) )
| ~ ( B @ ( A @ '$ki_accessible' ) )
| ~ ( A @ sk7 )
| ~ ( A @ ( '$ki_local_world' @ '$ki_accessible' ) ) ),
inference(simp,[status(thm)],[1490]) ).
thf(45,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ implies_3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_implies_3) ).
thf(410,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ implies_3 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(27,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ modus_tollens ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_modus_tollens) ).
thf(262,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ modus_tollens ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(19,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_implies_and ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_implies_and) ).
thf(210,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ op_implies_and ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(9,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 @ and ) @ ( F @ ( B @ and ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_substitution_1) ).
thf(136,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 @ and ) @ ( F @ ( B @ and ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(38,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' ) )
=> ( B @ ( F @ is_a_theorem ) ) )
& ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( B @ ( F @ qmltpeq ) ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',is_a_theorem_substitution_1) ).
thf(358,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' ) )
=> ( B @ ( F @ is_a_theorem ) ) )
& ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( B @ ( F @ qmltpeq ) ) ) ) )
=> ! [F: '$ki_world'] :
( ( F @ ( E @ '$ki_accessible' ) )
=> ( D @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(59,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ and_1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_and_1) ).
thf(532,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ and_1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(66,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ or_3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_3) ).
thf(596,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( A @ or_3 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
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: $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 @ equiv ) @ ( F @ ( B @ equiv ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equiv_substitution_1) ).
thf(200,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 @ equiv ) @ ( F @ ( B @ equiv ) @ ( H @ qmltpeq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(65,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(592,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)],[65]) ).
thf(54,axiom,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_and ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ not @ ( C @ not @ or ) @ not @ ( E @ ( C @ and ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_and_0) ).
thf(496,plain,
! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ op_and ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( E @ not @ ( C @ not @ or ) @ not @ ( E @ ( C @ and ) @ ( F @ qmltpeq ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(39,axiom,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r3_0) ).
thf(364,plain,
( ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r3 ) ) ) )
& ! [A: '$ki_world'] :
( ( A @ ( '$ki_local_world' @ '$ki_accessible' ) )
=> ( ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ( B @ r3 ) )
=> ! [B: '$ki_world'] :
( ( B @ ( A @ '$ki_accessible' ) )
=> ! [C: $i] :
( ( C @ ( B @ '$ki_exists_in_world_$i' ) )
=> ! [D: '$ki_world'] :
( ( D @ ( B @ '$ki_accessible' ) )
=> ! [E: $i] :
( ( E @ ( D @ '$ki_exists_in_world_$i' ) )
=> ! [F: '$ki_world'] :
( ( F @ ( D @ '$ki_accessible' ) )
=> ( C @ ( E @ or ) @ ( E @ ( C @ or ) @ implies ) @ ( F @ is_a_theorem ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(13960,plain,
$false,
inference(e,[status(thm)],[404,622,306,310,158,75,1036,88,408,308,120,440,550,142,500,1342,570,460,969,78,106,966,492,164,89,116,428,206,312,74,380,220,534,260,598,70,693,566,97,522,224,476,526,212,73,244,266,530,412,618,264,180,444,402,286,204,382,572,900,76,494,1339,140,240,330,162,342,72,314,495,218,2302,410,262,210,136,358,532,596,200,90,592,496,364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.39 % Computer : n019.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Fri Sep 25 23:50:49 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.77/0.89 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.21/1.31 % [INFO] Parsing done (408ms).
% 2.21/1.32 % [INFO] Running in sequential loop mode.
% 2.72/1.69 % [INFO] eprover registered as external prover.
% 2.90/1.70 % [INFO] Scanning for conjecture ...
% 3.09/1.86 % [INFO] Found a conjecture (or negated_conjecture) and 67 axioms. Running axiom selection ...
% 3.27/1.97 % [INFO] Axiom selection finished. Selected 67 axioms (removed 0 axioms).
% 4.06/2.24 % [INFO] Problem is typed first-order (TPTP TFF).
% 4.06/2.27 % [INFO] Type checking passed.
% 4.06/2.28 % [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 ...
% 147.30/84.90 % External prover 'e' found a proof!
% 147.30/84.90 % [INFO] Killing All external provers ...
% 147.30/84.90 % Time passed: 84409ms (effective reasoning time: 83575ms)
% 147.30/84.90 % 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)>
% 147.30/84.90 % Axioms used in derivation (67): implies_2_0, equiv_substitution_1, equivalence_2_0, kn1_0, implies_3_0, op_and_0, $ki_exists_in_world_$i_nonempty, principia_op_and, substitution_of_equivalents_1, r3_0, equiv_substitution_2, or_substitution_2, implies_substitution_2, r4_0, op_equiv_0, op_implies_or_0, hilbert_implies_1, hilbert_and_3, hilbert_op_implies_and, op_implies_and_0, substitution_of_equivalents_0, mrel_reflexive, and_substitution_2, or_1_0, cn3_0, and_3_0, cn2_0, modus_ponens_0, hilbert_or_1, kn2_0, principia_op_equiv, reflexivity, modus_tollens_0, hilbert_or_2, hilbert_implies_2, equivalence_3_0, or_2_0, hilbert_and_2, not_substitution_1, hilbert_modus_tollens, hilbert_op_or, implies_1_0, hilbert_equivalence_2, cn1_0, hilbert_equivalence_3, hilbert_modus_ponens, hilbert_implies_3, is_a_theorem_substitution_1, and_substitution_1, hilbert_and_1, and_2_0, op_or_0, hilbert_equivalence_1, hilbert_or_3, and_1_0, transitivity, r1_0, r2_0, or_substitution_1, r5_0, implies_substitution_1, kn3_0, equivalence_1_0, hilbert_op_equiv, or_3_0, symmetry, principia_op_implies_or
% 147.30/84.90 % No. of inferences in proof: 177
% 147.30/84.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 84409 ms resp. 83575 ms w/o parsing
% 147.98/85.16 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 147.98/85.16 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------