%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SWV433^2 : TPTP v9.2.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 09:45:19 AM UTC 2026
% Result : Unknown 2.06s 1.55s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SWV433^2 : TPTP v9.2.1. Released v3.6.0.
% 0.00/0.10 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.30 % Computer : n015.cluster.edu
% 0.13/0.30 % Model : x86_64 x86_64
% 0.13/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.30 % Memory : 8042.1875MB
% 0.13/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.30 % CPULimit : 300
% 0.13/0.30 % WCLimit : 300
% 0.13/0.30 % DateTime : Tue Feb 24 13:23:31 EST 2026
% 0.13/0.31 % CPUTime :
% 0.13/0.31 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.39 ---- Original DTF file ---
% 0.18/0.40 thf(spec,logic,$$dhol).
% 0.18/0.40 %------------------------------------------------------------------------------
% 0.18/0.40 % File : SWV433^2 : TPTP v9.2.1. Released v3.6.0.
% 0.18/0.40 % Domain : Software Verification (Security)
% 0.18/0.40 % Problem : ICL^=> logic mapping to modal logic implies that Example 2 holds
% 0.18/0.40 % Version : [Ben08] axioms : Augmented.
% 0.18/0.40 % English :
% 0.18/0.40
% 0.18/0.40 % Refs : [GA08] Garg & Abadi (2008), A Modal Deconstruction of Access
% 0.18/0.40 % : [Ben08] Benzmueller (2008), Automating Access Control Logics i
% 0.18/0.40 % : [BP09] Benzmueller & Paulson (2009), Exploring Properties of
% 0.18/0.40 % Source : [Ben08]
% 0.18/0.40 % Names :
% 0.18/0.40
% 0.18/0.40 % Status : Theorem
% 0.18/0.40 % Rating : 0.44 v9.1.0, 0.38 v9.0.0, 0.70 v8.2.0, 0.77 v8.1.0, 0.73 v7.5.0, 0.57 v7.4.0, 0.67 v7.2.0, 0.62 v7.0.0, 0.57 v6.4.0, 0.50 v6.3.0, 0.60 v6.2.0, 0.86 v6.1.0, 0.71 v5.5.0, 1.00 v5.4.0, 0.60 v5.3.0, 0.80 v5.1.0, 1.00 v5.0.0, 0.80 v4.1.0, 0.67 v3.7.0
% 0.18/0.40 % Syntax : Number of formulae : 67 ( 25 unt; 35 typ; 25 def)
% 0.18/0.40 % Number of atoms : 124 ( 25 equ; 0 cnn)
% 0.18/0.40 % Maximal formula atoms : 12 ( 3 avg)
% 0.18/0.40 % Number of connectives : 102 ( 3 ~; 1 |; 2 &; 95 @)
% 0.18/0.40 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 0.18/0.40 % Maximal formula depth : 8 ( 2 avg)
% 0.18/0.40 % Number of types : 3 ( 1 usr)
% 0.18/0.40 % Number of type conns : 135 ( 135 >; 0 *; 0 +; 0 <<)
% 0.18/0.40 % Number of symbols : 43 ( 40 usr; 9 con; 0-3 aty)
% 0.18/0.40 % Number of variables : 51 ( 41 ^; 6 !; 4 ?; 51 :)
% 0.18/0.40 % SPC : TH0_THM_EQU_NAR
% 0.18/0.40
% 0.18/0.40 % Comments :
% 0.18/0.40 %------------------------------------------------------------------------------
% 0.18/0.40 %----Include axioms of multi modal logic
% 0.18/0.40 include('Axioms/LCL008^0.ax').
% 0.18/0.40 %----Include axioms of ICL logic
% 0.18/0.40 include('Axioms/SWV008^0.ax').
% 0.18/0.40 %----Include axioms for ICL notions of validity wrt S4
% 0.18/0.40 include('Axioms/SWV008^1.ax').
% 0.18/0.40 %----Include axioms of ICL^=> logic
% 0.18/0.40 include('Axioms/SWV008^2.ax').
% 0.18/0.40 %------------------------------------------------------------------------------
% 0.18/0.40 %----The prinicpals
% 0.18/0.40 thf(admin,type,
% 0.18/0.40 admin: $i > $o ).
% 0.18/0.40
% 0.18/0.40 thf(bob,type,
% 0.18/0.40 bob: $i > $o ).
% 0.18/0.40
% 0.18/0.40 thf(alice,type,
% 0.18/0.40 alice: $i > $o ).
% 0.18/0.40
% 0.18/0.40 %----The atoms
% 0.18/0.40 thf(deletfile1,type,
% 0.18/0.40 deletefile1: $i > $o ).
% 0.18/0.40
% 0.18/0.40 %----The axioms of the example problem
% 0.18/0.40 %----(admin says deletefile1) => deletfile1
% 0.18/0.40 thf(ax1,axiom,
% 0.18/0.40 iclval @ ( icl_impl @ ( icl_says @ ( icl_princ @ admin ) @ ( icl_atom @ deletefile1 ) ) @ ( icl_atom @ deletefile1 ) ) ).
% 0.18/0.40
% 0.18/0.40 %----(admin says ((bob says deletefile1) => deletfile1))
% 0.18/0.40 thf(ax2,axiom,
% 0.18/0.40 iclval @ ( icl_says @ ( icl_princ @ admin ) @ ( icl_impl @ ( icl_says @ ( icl_princ @ bob ) @ ( icl_atom @ deletefile1 ) ) @ ( icl_atom @ deletefile1 ) ) ) ).
% 0.18/0.40
% 0.18/0.40 %----(bob says (alice ==> bob))
% 0.18/0.40 thf(ax3,axiom,
% 0.18/0.40 iclval @ ( icl_says @ ( icl_princ @ bob ) @ ( icl_impl_princ @ ( icl_princ @ alice ) @ ( icl_princ @ bob ) ) ) ).
% 0.18/0.40
% 0.18/0.40 %----(alice says deletefile1)
% 0.18/0.40 thf(ax4,axiom,
% 0.18/0.40 iclval @ ( icl_says @ ( icl_princ @ alice ) @ ( icl_atom @ deletefile1 ) ) ).
% 0.18/0.40
% 0.18/0.40 %----We prove deletefile1
% 0.18/0.40 thf(conj,conjecture,
% 0.18/0.40 iclval @ ( icl_atom @ deletefile1 ) ).
% 0.18/0.40
% 0.18/0.40 %------------------------------------------------------------------------------
% 0.18/0.40 ------------------------
% 2.06/1.52 ---- Embedded in THF ---
% 2.06/1.52 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 2.06/1.52 %%% Generated on Tue Feb 24 13:23:32 EST 2026
% 2.06/1.52 %%% using '$$dhol' embedding, version 1.3.0.
% 2.06/1.52 %%% Logic specification used:
% 2.06/1.52 %%% thf(spec, logic, $$dhol).
% 2.06/1.52
% 2.06/1.52 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.L4MNiR8XYa/DTF2DTF3462.p
% 2.06/1.52 thf(prop_a, type, prop_a: ($i > $o)).
% 2.06/1.52 thf(prop_b, type, prop_b: ($i > $o)).
% 2.06/1.52 thf(prop_c, type, prop_c: ($i > $o)).
% 2.06/1.52 thf(mfalse_decl, type, mfalse: ($i > $o)).
% 2.06/1.52 thf(mfalse, definition, (mfalse = (^ [X:$i]: ($false)))).
% 2.06/1.52 thf(mtrue_decl, type, mtrue: ($i > $o)).
% 2.06/1.52 thf(mtrue, definition, (mtrue = (^ [X:$i]: ($true)))).
% 2.06/1.52 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 2.06/1.52 thf(mnot, definition, (mnot = (^ [X:($i > $o),U:$i]: ((~ ((X @ U))))))).
% 2.06/1.52 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(mor, definition, (mor = (^ [X:($i > $o),Y:($i > $o),U:$i]: (((X @ U) | (Y @ U)))))).
% 2.06/1.52 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(mand, definition, (mand = (^ [X:($i > $o),Y:($i > $o),U:$i]: (((X @ U) & (Y @ U)))))).
% 2.06/1.52 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(mimpl, definition, (mimpl = (^ [U:($i > $o),V:($i > $o)]: (((mor @ (mnot @ U)) @ V))))).
% 2.06/1.52 thf(miff_decl, type, miff: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(miff, definition, (miff = (^ [U:($i > $o),V:($i > $o)]: (((mand @ ((mimpl @ U) @ V)) @ ((mimpl @ V) @ U)))))).
% 2.06/1.52 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(mbox, definition, (mbox = (^ [R:($i > ($i > $o)),P:($i > $o),X:$i]: ((! [Y:$i]: ((((R @ X) @ Y) => (P @ Y)))))))).
% 2.06/1.52 thf(mdia_decl, type, mdia: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(mdia, definition, (mdia = (^ [R:($i > ($i > $o)),P:($i > $o),X:$i]: ((? [Y:$i]: ((((R @ X) @ Y) & (P @ Y)))))))).
% 2.06/1.52 thf(individuals_decl, type, individuals: $tType).
% 2.06/1.52 thf(mall_decl, type, mall: ((individuals > ($i > $o)) > ($i > $o))).
% 2.06/1.52 thf(mall, definition, (mall = (^ [P:(individuals > ($i > $o)),W:$i]: ((! [X:individuals]: (((P @ X) @ W))))))).
% 2.06/1.52 thf(mexists_decl, type, mexists: ((individuals > ($i > $o)) > ($i > $o))).
% 2.06/1.52 thf(mexists, definition, (mexists = (^ [P:(individuals > ($i > $o)),W:$i]: ((? [X:individuals]: (((P @ X) @ W))))))).
% 2.06/1.52 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 2.06/1.52 thf(mvalid, definition, (mvalid = (^ [P:($i > $o)]: ((! [W:$i]: ((P @ W))))))).
% 2.06/1.52 thf(msatisfiable_decl, type, msatisfiable: (($i > $o) > $o)).
% 2.06/1.52 thf(msatisfiable, definition, (msatisfiable = (^ [P:($i > $o)]: ((? [W:$i]: ((P @ W))))))).
% 2.06/1.52 thf(mcountersatisfiable_decl, type, mcountersatisfiable: (($i > $o) > $o)).
% 2.06/1.52 thf(mcountersatisfiable, definition, (mcountersatisfiable = (^ [P:($i > $o)]: ((? [W:$i]: ((~ ((P @ W))))))))).
% 2.06/1.52 thf(minvalid_decl, type, minvalid: (($i > $o) > $o)).
% 2.06/1.52 thf(minvalid, definition, (minvalid = (^ [P:($i > $o)]: ((! [W:$i]: ((~ ((P @ W))))))))).
% 2.06/1.52 thf(rel_type, type, rel: ($i > ($i > $o))).
% 2.06/1.52 thf(icl_atom_type, type, icl_atom: (($i > $o) > ($i > $o))).
% 2.06/1.52 thf(icl_atom, definition, (icl_atom = (^ [P:($i > $o)]: (((mbox @ rel) @ P))))).
% 2.06/1.52 thf(icl_princ_type, type, icl_princ: (($i > $o) > ($i > $o))).
% 2.06/1.52 thf(icl_princ, definition, (icl_princ = (^ [P:($i > $o)]: (P)))).
% 2.06/1.52 thf(icl_and_type, type, icl_and: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(icl_and, definition, (icl_and = (^ [A:($i > $o),B:($i > $o)]: (((mand @ A) @ B))))).
% 2.06/1.52 thf(icl_or_type, type, icl_or: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(icl_or, definition, (icl_or = (^ [A:($i > $o),B:($i > $o)]: (((mor @ A) @ B))))).
% 2.06/1.52 thf(icl_impl_type, type, icl_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(icl_impl, definition, (icl_impl = (^ [A:($i > $o),B:($i > $o)]: (((mbox @ rel) @ ((mimpl @ A) @ B)))))).
% 2.06/1.52 thf(icl_true_type, type, icl_true: ($i > $o)).
% 2.06/1.52 thf(icl_true, definition, (icl_true = mtrue)).
% 2.06/1.52 thf(icl_false_type, type, icl_false: ($i > $o)).
% 2.06/1.52 thf(icl_false, definition, (icl_false = mfalse)).
% 2.06/1.52 thf(icl_says_type, type, icl_says: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(icl_says, definition, (icl_says = (^ [A:($i > $o),S:($i > $o)]: (((mbox @ rel) @ ((mor @ A) @ S)))))).
% 2.06/1.52 thf(iclval_decl_type, type, iclval: (($i > $o) > $o)).
% 2.06/1.52 thf(icl_s4_valid, definition, (iclval = (^ [X:($i > $o)]: ((mvalid @ X))))).
% 2.06/1.52 thf(refl_axiom, axiom, (! [A:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ rel) @ A)) @ A))))).
% 2.06/1.52 thf(trans_axiom, axiom, (! [B:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ rel) @ B)) @ ((mbox @ rel) @ ((mbox @ rel) @ B))))))).
% 2.06/1.52 thf(icl_impl_princ_type, type, icl_impl_princ: (($i > $o) > (($i > $o) > ($i > $o)))).
% 2.06/1.52 thf(icl_impl_princ, definition, (icl_impl_princ = (^ [A:($i > $o),B:($i > $o)]: (((mbox @ rel) @ ((mimpl @ A) @ B)))))).
% 2.06/1.52 thf(spec, logic, $$dhol).
% 2.06/1.52 thf(admin, type, admin: ($i > $o)).
% 2.06/1.52 thf(bob, type, bob: ($i > $o)).
% 2.06/1.52 thf(alice, type, alice: ($i > $o)).
% 2.06/1.52 thf(deletfile1, type, deletefile1: ($i > $o)).
% 2.06/1.52 thf(ax1, axiom, (iclval @ ((icl_impl @ ((icl_says @ (icl_princ @ admin)) @ (icl_atom @ deletefile1))) @ (icl_atom @ deletefile1)))).
% 2.06/1.52 thf(ax2, axiom, (iclval @ ((icl_says @ (icl_princ @ admin)) @ ((icl_impl @ ((icl_says @ (icl_princ @ bob)) @ (icl_atom @ deletefile1))) @ (icl_atom @ deletefile1))))).
% 2.06/1.52 thf(ax3, axiom, (iclval @ ((icl_says @ (icl_princ @ bob)) @ ((icl_impl_princ @ (icl_princ @ alice)) @ (icl_princ @ bob))))).
% 2.06/1.52 thf(ax4, axiom, (iclval @ ((icl_says @ (icl_princ @ alice)) @ (icl_atom @ deletefile1)))).
% 2.06/1.52 thf(conj, conjecture, (iclval @ (icl_atom @ deletefile1))).
% 2.06/1.52 % SZS output end ListOfTHF for /export/starexec/sandbox/tmp/tmp.L4MNiR8XYa/DTF2DTF3462.p
% 2.06/1.52 ------------------------
% 2.06/1.53 ---- Cleaned THF ---
% 2.06/1.53 thf(prop_a,type,
% 2.06/1.53 prop_a: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(prop_b,type,
% 2.06/1.53 prop_b: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(prop_c,type,
% 2.06/1.53 prop_c: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mfalse_decl,type,
% 2.06/1.53 mfalse: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mfalse,definition,
% 2.06/1.53 ( mfalse
% 2.06/1.53 = ( ^ [X: $i] : $false ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mtrue_decl,type,
% 2.06/1.53 mtrue: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mtrue,definition,
% 2.06/1.53 ( mtrue
% 2.06/1.53 = ( ^ [X: $i] : $true ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mnot_decl,type,
% 2.06/1.53 mnot: ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mnot,definition,
% 2.06/1.53 ( mnot
% 2.06/1.53 = ( ^ [X: $i > $o,U: $i] :
% 2.06/1.53 ~ ( X @ U ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mor_decl,type,
% 2.06/1.53 mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mor,definition,
% 2.06/1.53 ( mor
% 2.06/1.53 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 2.06/1.53 ( ( X @ U )
% 2.06/1.53 | ( Y @ U ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mand_decl,type,
% 2.06/1.53 mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mand,definition,
% 2.06/1.53 ( mand
% 2.06/1.53 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 2.06/1.53 ( ( X @ U )
% 2.06/1.53 & ( Y @ U ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mimpl_decl,type,
% 2.06/1.53 mimpl: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mimpl,definition,
% 2.06/1.53 ( mimpl
% 2.06/1.53 = ( ^ [U: $i > $o,V: $i > $o] : ( mor @ ( mnot @ U ) @ V ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(miff_decl,type,
% 2.06/1.53 miff: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(miff,definition,
% 2.06/1.53 ( miff
% 2.06/1.53 = ( ^ [U: $i > $o,V: $i > $o] : ( mand @ ( mimpl @ U @ V ) @ ( mimpl @ V @ U ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mbox_decl,type,
% 2.06/1.53 mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mbox,definition,
% 2.06/1.53 ( mbox
% 2.06/1.53 = ( ^ [R: $i > $i > $o,P: $i > $o,X: $i] :
% 2.06/1.53 ! [Y: $i] :
% 2.06/1.53 ( ( R @ X @ Y )
% 2.06/1.53 => ( P @ Y ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mdia_decl,type,
% 2.06/1.53 mdia: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mdia,definition,
% 2.06/1.53 ( mdia
% 2.06/1.53 = ( ^ [R: $i > $i > $o,P: $i > $o,X: $i] :
% 2.06/1.53 ? [Y: $i] :
% 2.06/1.53 ( ( R @ X @ Y )
% 2.06/1.53 & ( P @ Y ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(individuals_decl,type,
% 2.06/1.53 individuals: $tType ).
% 2.06/1.53
% 2.06/1.53 thf(mall_decl,type,
% 2.06/1.53 mall: ( individuals > $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mall,definition,
% 2.06/1.53 ( mall
% 2.06/1.53 = ( ^ [P: individuals > $i > $o,W: $i] :
% 2.06/1.53 ! [X: individuals] : ( P @ X @ W ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mexists_decl,type,
% 2.06/1.53 mexists: ( individuals > $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mexists,definition,
% 2.06/1.53 ( mexists
% 2.06/1.53 = ( ^ [P: individuals > $i > $o,W: $i] :
% 2.06/1.53 ? [X: individuals] : ( P @ X @ W ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mvalid_decl,type,
% 2.06/1.53 mvalid: ( $i > $o ) > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mvalid,definition,
% 2.06/1.53 ( mvalid
% 2.06/1.53 = ( ^ [P: $i > $o] :
% 2.06/1.53 ! [W: $i] : ( P @ W ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(msatisfiable_decl,type,
% 2.06/1.53 msatisfiable: ( $i > $o ) > $o ).
% 2.06/1.53
% 2.06/1.53 thf(msatisfiable,definition,
% 2.06/1.53 ( msatisfiable
% 2.06/1.53 = ( ^ [P: $i > $o] :
% 2.06/1.53 ? [W: $i] : ( P @ W ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(mcountersatisfiable_decl,type,
% 2.06/1.53 mcountersatisfiable: ( $i > $o ) > $o ).
% 2.06/1.53
% 2.06/1.53 thf(mcountersatisfiable,definition,
% 2.06/1.53 ( mcountersatisfiable
% 2.06/1.53 = ( ^ [P: $i > $o] :
% 2.06/1.53 ? [W: $i] :
% 2.06/1.53 ~ ( P @ W ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(minvalid_decl,type,
% 2.06/1.53 minvalid: ( $i > $o ) > $o ).
% 2.06/1.53
% 2.06/1.53 thf(minvalid,definition,
% 2.06/1.53 ( minvalid
% 2.06/1.53 = ( ^ [P: $i > $o] :
% 2.06/1.53 ! [W: $i] :
% 2.06/1.53 ~ ( P @ W ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(rel_type,type,
% 2.06/1.53 rel: $i > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_atom_type,type,
% 2.06/1.53 icl_atom: ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_atom,definition,
% 2.06/1.53 ( icl_atom
% 2.06/1.53 = ( ^ [P: $i > $o] : ( mbox @ rel @ P ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(icl_princ_type,type,
% 2.06/1.53 icl_princ: ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_princ,definition,
% 2.06/1.53 ( icl_princ
% 2.06/1.53 = ( ^ [P: $i > $o] : P ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(icl_and_type,type,
% 2.06/1.53 icl_and: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_and,definition,
% 2.06/1.53 ( icl_and
% 2.06/1.53 = ( ^ [A: $i > $o,B: $i > $o] : ( mand @ A @ B ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(icl_or_type,type,
% 2.06/1.53 icl_or: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_or,definition,
% 2.06/1.53 ( icl_or
% 2.06/1.53 = ( ^ [A: $i > $o,B: $i > $o] : ( mor @ A @ B ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(icl_impl_type,type,
% 2.06/1.53 icl_impl: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_impl,definition,
% 2.06/1.53 ( icl_impl
% 2.06/1.53 = ( ^ [A: $i > $o,B: $i > $o] : ( mbox @ rel @ ( mimpl @ A @ B ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(icl_true_type,type,
% 2.06/1.53 icl_true: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_true,definition,
% 2.06/1.53 icl_true = mtrue ).
% 2.06/1.53
% 2.06/1.53 thf(icl_false_type,type,
% 2.06/1.53 icl_false: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_false,definition,
% 2.06/1.53 icl_false = mfalse ).
% 2.06/1.53
% 2.06/1.53 thf(icl_says_type,type,
% 2.06/1.53 icl_says: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_says,definition,
% 2.06/1.53 ( icl_says
% 2.06/1.53 = ( ^ [A: $i > $o,S: $i > $o] : ( mbox @ rel @ ( mor @ A @ S ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(iclval_decl_type,type,
% 2.06/1.53 iclval: ( $i > $o ) > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_s4_valid,definition,
% 2.06/1.53 ( iclval
% 2.06/1.53 = ( ^ [X: $i > $o] : ( mvalid @ X ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(refl_axiom,axiom,
% 2.06/1.53 ! [A: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ rel @ A ) @ A ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(trans_axiom,axiom,
% 2.06/1.53 ! [B: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ rel @ B ) @ ( mbox @ rel @ ( mbox @ rel @ B ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(icl_impl_princ_type,type,
% 2.06/1.53 icl_impl_princ: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(icl_impl_princ,definition,
% 2.06/1.53 ( icl_impl_princ
% 2.06/1.53 = ( ^ [A: $i > $o,B: $i > $o] : ( mbox @ rel @ ( mimpl @ A @ B ) ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(spec,logic,
% 2.06/1.53 $$dhol ).
% 2.06/1.53
% 2.06/1.53 thf(admin,type,
% 2.06/1.53 admin: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(bob,type,
% 2.06/1.53 bob: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(alice,type,
% 2.06/1.53 alice: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(deletfile1,type,
% 2.06/1.53 deletefile1: $i > $o ).
% 2.06/1.53
% 2.06/1.53 thf(ax1,axiom,
% 2.06/1.53 iclval @ ( icl_impl @ ( icl_says @ ( icl_princ @ admin ) @ ( icl_atom @ deletefile1 ) ) @ ( icl_atom @ deletefile1 ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(ax2,axiom,
% 2.06/1.53 iclval @ ( icl_says @ ( icl_princ @ admin ) @ ( icl_impl @ ( icl_says @ ( icl_princ @ bob ) @ ( icl_atom @ deletefile1 ) ) @ ( icl_atom @ deletefile1 ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(ax3,axiom,
% 2.06/1.53 iclval @ ( icl_says @ ( icl_princ @ bob ) @ ( icl_impl_princ @ ( icl_princ @ alice ) @ ( icl_princ @ bob ) ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(ax4,axiom,
% 2.06/1.53 iclval @ ( icl_says @ ( icl_princ @ alice ) @ ( icl_atom @ deletefile1 ) ) ).
% 2.06/1.53
% 2.06/1.53 thf(conj,conjecture,
% 2.06/1.53 iclval @ ( icl_atom @ deletefile1 ) ).
% 2.06/1.53 ------------------------
% 2.06/1.55 % Exception at proof search level
% 2.06/1.55 Parsing Error on line 214
% 2.06/1.55 unit type, such as axiom or definition expected but logic found at position 143
%------------------------------------------------------------------------------