%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SWV446^1 : TPTP v9.2.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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:21 AM UTC 2026
% Result : Unknown 1.83s 1.37s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV446^1 : TPTP v9.2.1. Released v3.7.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.34 % Computer : n007.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue Feb 24 13:23:08 EST 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.28/0.47 ---- Original DTF file ---
% 0.28/0.47 thf(spec,logic,$$dhol).
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 % File : SWV446^1 : TPTP v9.2.1. Released v3.7.0.
% 0.28/0.47 % Domain : Software Verification (Security)
% 0.28/0.47 % Problem : K says ((K says A) => A) in BL
% 0.28/0.47 % Version : [Gar08] axioms.
% 0.28/0.47 % English :
% 0.28/0.47
% 0.28/0.47 % Refs : [AM+01] Alechina et al. (2001), Categorical and Kripke Semanti
% 0.28/0.47 % : [Gar08] Garg (2008), Principal-Centric Reasoning in Constructi
% 0.28/0.47 % : [Gar09] Garg (2009), Email to Geoff Sutcliffe
% 0.28/0.47 % Source : [Gar09]
% 0.28/0.47 % Names :
% 0.28/0.47
% 0.28/0.47 % Status : Theorem
% 0.28/0.47 % Rating : 0.44 v9.1.0, 0.50 v8.2.0, 0.54 v8.1.0, 0.45 v7.5.0, 0.29 v7.4.0, 0.56 v7.2.0, 0.50 v7.0.0, 0.43 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.71 v6.1.0, 0.57 v6.0.0, 0.29 v5.5.0, 0.50 v5.4.0, 0.80 v4.1.0, 1.00 v3.7.0
% 0.28/0.47 % Syntax : Number of formulae : 84 ( 34 unt; 43 typ; 34 def)
% 0.28/0.47 % Number of atoms : 150 ( 34 equ; 0 cnn)
% 0.28/0.47 % Maximal formula atoms : 10 ( 3 avg)
% 0.28/0.47 % Number of connectives : 121 ( 3 ~; 1 |; 2 &; 114 @)
% 0.28/0.47 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 0.28/0.47 % Maximal formula depth : 9 ( 2 avg)
% 0.28/0.47 % Number of types : 3 ( 1 usr)
% 0.28/0.47 % Number of type conns : 175 ( 175 >; 0 *; 0 +; 0 <<)
% 0.28/0.47 % Number of symbols : 49 ( 46 usr; 8 con; 0-3 aty)
% 0.28/0.47 % Number of variables : 65 ( 50 ^; 11 !; 4 ?; 65 :)
% 0.28/0.47 % SPC : TH0_THM_EQU_NAR
% 0.28/0.47
% 0.28/0.47 % Comments :
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 %----Include axioms of multi-modal logic
% 0.28/0.47 include('Axioms/LCL008^0.ax').
% 0.28/0.47 %----Include axioms translating constructive S4 (CS4) to bimodal classical
% 0.28/0.47 %----S4 (BS4)
% 0.28/0.47 include('Axioms/LCL009^0.ax').
% 0.28/0.47 %----Include axioms for translation from Binder Logic (BL) to CS4
% 0.28/0.47 include('Axioms/SWV010^0.ax').
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 thf(bl_conceit,conjecture,
% 0.28/0.47 ! [K: individuals,A: $i > $o] : ( bl_valid @ ( bl_says @ K @ ( bl_impl @ ( bl_says @ K @ ( bl_atom @ A ) ) @ ( bl_atom @ A ) ) ) ) ).
% 0.28/0.47
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 ------------------------
% 1.83/1.33 ---- Embedded in THF ---
% 1.83/1.34 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.83/1.34 %%% Generated on Tue Feb 24 13:23:09 EST 2026
% 1.83/1.34 %%% using '$$dhol' embedding, version 1.3.0.
% 1.83/1.34 %%% Logic specification used:
% 1.83/1.34 %%% thf(spec, logic, $$dhol).
% 1.83/1.34
% 1.83/1.34 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.ZDhzWpCBEO/DTF2DTF22812.p
% 1.83/1.34 thf(prop_a, type, prop_a: ($i > $o)).
% 1.83/1.34 thf(prop_b, type, prop_b: ($i > $o)).
% 1.83/1.34 thf(prop_c, type, prop_c: ($i > $o)).
% 1.83/1.34 thf(mfalse_decl, type, mfalse: ($i > $o)).
% 1.83/1.34 thf(mfalse, definition, (mfalse = (^ [X:$i]: ($false)))).
% 1.83/1.34 thf(mtrue_decl, type, mtrue: ($i > $o)).
% 1.83/1.34 thf(mtrue, definition, (mtrue = (^ [X:$i]: ($true)))).
% 1.83/1.34 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 1.83/1.34 thf(mnot, definition, (mnot = (^ [X:($i > $o),U:$i]: ((~ ((X @ U))))))).
% 1.83/1.34 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(mor, definition, (mor = (^ [X:($i > $o),Y:($i > $o),U:$i]: (((X @ U) | (Y @ U)))))).
% 1.83/1.34 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(mand, definition, (mand = (^ [X:($i > $o),Y:($i > $o),U:$i]: (((X @ U) & (Y @ U)))))).
% 1.83/1.34 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(mimpl, definition, (mimpl = (^ [U:($i > $o),V:($i > $o)]: (((mor @ (mnot @ U)) @ V))))).
% 1.83/1.34 thf(miff_decl, type, miff: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(miff, definition, (miff = (^ [U:($i > $o),V:($i > $o)]: (((mand @ ((mimpl @ U) @ V)) @ ((mimpl @ V) @ U)))))).
% 1.83/1.34 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(mbox, definition, (mbox = (^ [R:($i > ($i > $o)),P:($i > $o),X:$i]: ((! [Y:$i]: ((((R @ X) @ Y) => (P @ Y)))))))).
% 1.83/1.34 thf(mdia_decl, type, mdia: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(mdia, definition, (mdia = (^ [R:($i > ($i > $o)),P:($i > $o),X:$i]: ((? [Y:$i]: ((((R @ X) @ Y) & (P @ Y)))))))).
% 1.83/1.34 thf(individuals_decl, type, individuals: $tType).
% 1.83/1.34 thf(mall_decl, type, mall: ((individuals > ($i > $o)) > ($i > $o))).
% 1.83/1.34 thf(mall, definition, (mall = (^ [P:(individuals > ($i > $o)),W:$i]: ((! [X:individuals]: (((P @ X) @ W))))))).
% 1.83/1.34 thf(mexists_decl, type, mexists: ((individuals > ($i > $o)) > ($i > $o))).
% 1.83/1.34 thf(mexists, definition, (mexists = (^ [P:(individuals > ($i > $o)),W:$i]: ((? [X:individuals]: (((P @ X) @ W))))))).
% 1.83/1.34 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 1.83/1.34 thf(mvalid, definition, (mvalid = (^ [P:($i > $o)]: ((! [W:$i]: ((P @ W))))))).
% 1.83/1.34 thf(msatisfiable_decl, type, msatisfiable: (($i > $o) > $o)).
% 1.83/1.34 thf(msatisfiable, definition, (msatisfiable = (^ [P:($i > $o)]: ((? [W:$i]: ((P @ W))))))).
% 1.83/1.34 thf(mcountersatisfiable_decl, type, mcountersatisfiable: (($i > $o) > $o)).
% 1.83/1.34 thf(mcountersatisfiable, definition, (mcountersatisfiable = (^ [P:($i > $o)]: ((? [W:$i]: ((~ ((P @ W))))))))).
% 1.83/1.34 thf(minvalid_decl, type, minvalid: (($i > $o) > $o)).
% 1.83/1.34 thf(minvalid, definition, (minvalid = (^ [P:($i > $o)]: ((! [W:$i]: ((~ ((P @ W))))))))).
% 1.83/1.34 thf(reli, type, reli: ($i > ($i > $o))).
% 1.83/1.34 thf(relr, type, relr: ($i > ($i > $o))).
% 1.83/1.34 thf(cs4_atom_decl, type, cs4_atom: (($i > $o) > ($i > $o))).
% 1.83/1.34 thf(cs4_and_decl, type, cs4_and: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(cs4_or_decl, type, cs4_or: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(cs4_impl_decl, type, cs4_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(cs4_true_decl, type, cs4_true: ($i > $o)).
% 1.83/1.34 thf(cs4_false_decl, type, cs4_false: ($i > $o)).
% 1.83/1.34 thf(cs4_all_decl, type, cs4_all: ((individuals > ($i > $o)) > ($i > $o))).
% 1.83/1.34 thf(cs4_box_decl, type, cs4_box: (($i > $o) > ($i > $o))).
% 1.83/1.34 thf(cs4_atom, definition, (cs4_atom = (^ [P:($i > $o)]: (((mbox @ reli) @ P))))).
% 1.83/1.34 thf(cs4_and, definition, (cs4_and = (^ [A:($i > $o),B:($i > $o)]: (((mand @ A) @ B))))).
% 1.83/1.34 thf(cs4_or, definition, (cs4_or = (^ [A:($i > $o),B:($i > $o)]: (((mor @ A) @ B))))).
% 1.83/1.34 thf(cs4_impl, definition, (cs4_impl = (^ [A:($i > $o),B:($i > $o)]: (((mbox @ reli) @ ((mimpl @ A) @ B)))))).
% 1.83/1.34 thf(cs4_true, definition, (cs4_true = mtrue)).
% 1.83/1.34 thf(cs4_false, definition, (cs4_false = mfalse)).
% 1.83/1.34 thf(cs4_all, definition, (cs4_all = (^ [A:(individuals > ($i > $o))]: (((mbox @ reli) @ (mall @ A)))))).
% 1.83/1.34 thf(cs4_box, definition, (cs4_box = (^ [A:($i > $o)]: (((mbox @ reli) @ ((mbox @ relr) @ A)))))).
% 1.83/1.34 thf(cs4_valid_decl, type, cs4_valid: (($i > $o) > $o)).
% 1.83/1.34 thf(cs4_valid_def, definition, (cs4_valid = (^ [A:($i > $o)]: ((mvalid @ A))))).
% 1.83/1.34 thf(refl_axiom_i, axiom, (! [A:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ reli) @ A)) @ A))))).
% 1.83/1.34 thf(refl_axiom_r, axiom, (! [A:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ relr) @ A)) @ A))))).
% 1.83/1.34 thf(trans_axiom_i, axiom, (! [A:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ reli) @ A)) @ ((mbox @ reli) @ ((mbox @ reli) @ A))))))).
% 1.83/1.34 thf(trans_axiom_r, axiom, (! [A:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ relr) @ A)) @ ((mbox @ relr) @ ((mbox @ relr) @ A))))))).
% 1.83/1.34 thf(ax_i_r_commute, axiom, (! [A:($i > $o)]: ((mvalid @ ((mimpl @ ((mbox @ reli) @ ((mbox @ relr) @ A))) @ ((mbox @ relr) @ ((mbox @ reli) @ A))))))).
% 1.83/1.34 thf(princ_inj, type, princ_inj: (individuals > ($i > $o))).
% 1.83/1.34 thf(bl_atom_decl, type, bl_atom: (($i > $o) > ($i > $o))).
% 1.83/1.34 thf(bl_princ_decl, type, bl_princ: (($i > $o) > ($i > $o))).
% 1.83/1.34 thf(bl_and_decl, type, bl_and: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(bl_or_decl, type, bl_or: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(bl_impl_decl, type, bl_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(bl_all_decl, type, bl_all: ((individuals > ($i > $o)) > ($i > $o))).
% 1.83/1.34 thf(bl_true_decl, type, bl_true: ($i > $o)).
% 1.83/1.34 thf(bl_false_decl, type, bl_false: ($i > $o)).
% 1.83/1.34 thf(bl_says_decl, type, bl_says: (individuals > (($i > $o) > ($i > $o)))).
% 1.83/1.34 thf(bl_atom, definition, (bl_atom = (^ [P:($i > $o)]: ((cs4_atom @ P))))).
% 1.83/1.34 thf(bl_princ, definition, (bl_princ = (^ [P:($i > $o)]: ((cs4_atom @ P))))).
% 1.83/1.34 thf(bl_and, definition, (bl_and = (^ [A:($i > $o),B:($i > $o)]: (((cs4_and @ A) @ B))))).
% 1.83/1.34 thf(bl_or, definition, (bl_or = (^ [A:($i > $o),B:($i > $o)]: (((cs4_or @ A) @ B))))).
% 1.83/1.34 thf(bl_impl, definition, (bl_impl = (^ [A:($i > $o),B:($i > $o)]: (((cs4_impl @ A) @ B))))).
% 1.83/1.34 thf(bl_all, definition, (bl_all = (^ [A:(individuals > ($i > $o))]: ((cs4_all @ A))))).
% 1.83/1.34 thf(bl_true, definition, (bl_true = cs4_true)).
% 1.83/1.34 thf(bl_false, definition, (bl_false = cs4_false)).
% 1.83/1.34 thf(bl_says, definition, (bl_says = (^ [K:individuals,A:($i > $o)]: ((cs4_box @ ((cs4_impl @ (bl_princ @ (princ_inj @ K))) @ A)))))).
% 1.83/1.34 thf(bl_valid_decl, type, bl_valid: (($i > $o) > $o)).
% 1.83/1.34 thf(bl_valid_def, definition, (bl_valid = mvalid)).
% 1.83/1.34 thf(loca_decl, type, loca: individuals).
% 1.83/1.34 thf(loca_strength, axiom, (cs4_valid @ (cs4_all @ (^ [K:individuals]: (((cs4_impl @ (princ_inj @ K)) @ (princ_inj @ loca))))))).
% 1.83/1.34 thf(spec, logic, $$dhol).
% 1.83/1.34 thf(bl_conceit, conjecture, (! [K:individuals,A:($i > $o)]: ((bl_valid @ ((bl_says @ K) @ ((bl_impl @ ((bl_says @ K) @ (bl_atom @ A))) @ (bl_atom @ A))))))).
% 1.83/1.34 % SZS output end ListOfTHF for /export/starexec/sandbox2/tmp/tmp.ZDhzWpCBEO/DTF2DTF22812.p
% 1.83/1.34 ------------------------
% 1.83/1.35 ---- Cleaned THF ---
% 1.83/1.35 thf(prop_a,type,
% 1.83/1.35 prop_a: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(prop_b,type,
% 1.83/1.35 prop_b: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(prop_c,type,
% 1.83/1.35 prop_c: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mfalse_decl,type,
% 1.83/1.35 mfalse: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mfalse,definition,
% 1.83/1.35 ( mfalse
% 1.83/1.35 = ( ^ [X: $i] : $false ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mtrue_decl,type,
% 1.83/1.35 mtrue: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mtrue,definition,
% 1.83/1.35 ( mtrue
% 1.83/1.35 = ( ^ [X: $i] : $true ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mnot_decl,type,
% 1.83/1.35 mnot: ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mnot,definition,
% 1.83/1.35 ( mnot
% 1.83/1.35 = ( ^ [X: $i > $o,U: $i] :
% 1.83/1.35 ~ ( X @ U ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mor_decl,type,
% 1.83/1.35 mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mor,definition,
% 1.83/1.35 ( mor
% 1.83/1.35 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 1.83/1.35 ( ( X @ U )
% 1.83/1.35 | ( Y @ U ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mand_decl,type,
% 1.83/1.35 mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mand,definition,
% 1.83/1.35 ( mand
% 1.83/1.35 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 1.83/1.35 ( ( X @ U )
% 1.83/1.35 & ( Y @ U ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mimpl_decl,type,
% 1.83/1.35 mimpl: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mimpl,definition,
% 1.83/1.35 ( mimpl
% 1.83/1.35 = ( ^ [U: $i > $o,V: $i > $o] : ( mor @ ( mnot @ U ) @ V ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(miff_decl,type,
% 1.83/1.35 miff: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(miff,definition,
% 1.83/1.35 ( miff
% 1.83/1.35 = ( ^ [U: $i > $o,V: $i > $o] : ( mand @ ( mimpl @ U @ V ) @ ( mimpl @ V @ U ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mbox_decl,type,
% 1.83/1.35 mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mbox,definition,
% 1.83/1.35 ( mbox
% 1.83/1.35 = ( ^ [R: $i > $i > $o,P: $i > $o,X: $i] :
% 1.83/1.35 ! [Y: $i] :
% 1.83/1.35 ( ( R @ X @ Y )
% 1.83/1.35 => ( P @ Y ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mdia_decl,type,
% 1.83/1.35 mdia: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mdia,definition,
% 1.83/1.35 ( mdia
% 1.83/1.35 = ( ^ [R: $i > $i > $o,P: $i > $o,X: $i] :
% 1.83/1.35 ? [Y: $i] :
% 1.83/1.35 ( ( R @ X @ Y )
% 1.83/1.35 & ( P @ Y ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(individuals_decl,type,
% 1.83/1.35 individuals: $tType ).
% 1.83/1.35
% 1.83/1.35 thf(mall_decl,type,
% 1.83/1.35 mall: ( individuals > $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mall,definition,
% 1.83/1.35 ( mall
% 1.83/1.35 = ( ^ [P: individuals > $i > $o,W: $i] :
% 1.83/1.35 ! [X: individuals] : ( P @ X @ W ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mexists_decl,type,
% 1.83/1.35 mexists: ( individuals > $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mexists,definition,
% 1.83/1.35 ( mexists
% 1.83/1.35 = ( ^ [P: individuals > $i > $o,W: $i] :
% 1.83/1.35 ? [X: individuals] : ( P @ X @ W ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mvalid_decl,type,
% 1.83/1.35 mvalid: ( $i > $o ) > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mvalid,definition,
% 1.83/1.35 ( mvalid
% 1.83/1.35 = ( ^ [P: $i > $o] :
% 1.83/1.35 ! [W: $i] : ( P @ W ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(msatisfiable_decl,type,
% 1.83/1.35 msatisfiable: ( $i > $o ) > $o ).
% 1.83/1.35
% 1.83/1.35 thf(msatisfiable,definition,
% 1.83/1.35 ( msatisfiable
% 1.83/1.35 = ( ^ [P: $i > $o] :
% 1.83/1.35 ? [W: $i] : ( P @ W ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(mcountersatisfiable_decl,type,
% 1.83/1.35 mcountersatisfiable: ( $i > $o ) > $o ).
% 1.83/1.35
% 1.83/1.35 thf(mcountersatisfiable,definition,
% 1.83/1.35 ( mcountersatisfiable
% 1.83/1.35 = ( ^ [P: $i > $o] :
% 1.83/1.35 ? [W: $i] :
% 1.83/1.35 ~ ( P @ W ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(minvalid_decl,type,
% 1.83/1.35 minvalid: ( $i > $o ) > $o ).
% 1.83/1.35
% 1.83/1.35 thf(minvalid,definition,
% 1.83/1.35 ( minvalid
% 1.83/1.35 = ( ^ [P: $i > $o] :
% 1.83/1.35 ! [W: $i] :
% 1.83/1.35 ~ ( P @ W ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(reli,type,
% 1.83/1.35 reli: $i > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(relr,type,
% 1.83/1.35 relr: $i > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_atom_decl,type,
% 1.83/1.35 cs4_atom: ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_and_decl,type,
% 1.83/1.35 cs4_and: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_or_decl,type,
% 1.83/1.35 cs4_or: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_impl_decl,type,
% 1.83/1.35 cs4_impl: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_true_decl,type,
% 1.83/1.35 cs4_true: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_false_decl,type,
% 1.83/1.35 cs4_false: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_all_decl,type,
% 1.83/1.35 cs4_all: ( individuals > $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_box_decl,type,
% 1.83/1.35 cs4_box: ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_atom,definition,
% 1.83/1.35 ( cs4_atom
% 1.83/1.35 = ( ^ [P: $i > $o] : ( mbox @ reli @ P ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_and,definition,
% 1.83/1.35 ( cs4_and
% 1.83/1.35 = ( ^ [A: $i > $o,B: $i > $o] : ( mand @ A @ B ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_or,definition,
% 1.83/1.35 ( cs4_or
% 1.83/1.35 = ( ^ [A: $i > $o,B: $i > $o] : ( mor @ A @ B ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_impl,definition,
% 1.83/1.35 ( cs4_impl
% 1.83/1.35 = ( ^ [A: $i > $o,B: $i > $o] : ( mbox @ reli @ ( mimpl @ A @ B ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_true,definition,
% 1.83/1.35 cs4_true = mtrue ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_false,definition,
% 1.83/1.35 cs4_false = mfalse ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_all,definition,
% 1.83/1.35 ( cs4_all
% 1.83/1.35 = ( ^ [A: individuals > $i > $o] : ( mbox @ reli @ ( mall @ A ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_box,definition,
% 1.83/1.35 ( cs4_box
% 1.83/1.35 = ( ^ [A: $i > $o] : ( mbox @ reli @ ( mbox @ relr @ A ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_valid_decl,type,
% 1.83/1.35 cs4_valid: ( $i > $o ) > $o ).
% 1.83/1.35
% 1.83/1.35 thf(cs4_valid_def,definition,
% 1.83/1.35 ( cs4_valid
% 1.83/1.35 = ( ^ [A: $i > $o] : ( mvalid @ A ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(refl_axiom_i,axiom,
% 1.83/1.35 ! [A: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ reli @ A ) @ A ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(refl_axiom_r,axiom,
% 1.83/1.35 ! [A: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ relr @ A ) @ A ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(trans_axiom_i,axiom,
% 1.83/1.35 ! [A: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ reli @ A ) @ ( mbox @ reli @ ( mbox @ reli @ A ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(trans_axiom_r,axiom,
% 1.83/1.35 ! [A: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ relr @ A ) @ ( mbox @ relr @ ( mbox @ relr @ A ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(ax_i_r_commute,axiom,
% 1.83/1.35 ! [A: $i > $o] : ( mvalid @ ( mimpl @ ( mbox @ reli @ ( mbox @ relr @ A ) ) @ ( mbox @ relr @ ( mbox @ reli @ A ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(princ_inj,type,
% 1.83/1.35 princ_inj: individuals > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_atom_decl,type,
% 1.83/1.35 bl_atom: ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_princ_decl,type,
% 1.83/1.35 bl_princ: ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_and_decl,type,
% 1.83/1.35 bl_and: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_or_decl,type,
% 1.83/1.35 bl_or: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_impl_decl,type,
% 1.83/1.35 bl_impl: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_all_decl,type,
% 1.83/1.35 bl_all: ( individuals > $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_true_decl,type,
% 1.83/1.35 bl_true: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_false_decl,type,
% 1.83/1.35 bl_false: $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_says_decl,type,
% 1.83/1.35 bl_says: individuals > ( $i > $o ) > $i > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_atom,definition,
% 1.83/1.35 ( bl_atom
% 1.83/1.35 = ( ^ [P: $i > $o] : ( cs4_atom @ P ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_princ,definition,
% 1.83/1.35 ( bl_princ
% 1.83/1.35 = ( ^ [P: $i > $o] : ( cs4_atom @ P ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_and,definition,
% 1.83/1.35 ( bl_and
% 1.83/1.35 = ( ^ [A: $i > $o,B: $i > $o] : ( cs4_and @ A @ B ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_or,definition,
% 1.83/1.35 ( bl_or
% 1.83/1.35 = ( ^ [A: $i > $o,B: $i > $o] : ( cs4_or @ A @ B ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_impl,definition,
% 1.83/1.35 ( bl_impl
% 1.83/1.35 = ( ^ [A: $i > $o,B: $i > $o] : ( cs4_impl @ A @ B ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_all,definition,
% 1.83/1.35 ( bl_all
% 1.83/1.35 = ( ^ [A: individuals > $i > $o] : ( cs4_all @ A ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_true,definition,
% 1.83/1.35 bl_true = cs4_true ).
% 1.83/1.35
% 1.83/1.35 thf(bl_false,definition,
% 1.83/1.35 bl_false = cs4_false ).
% 1.83/1.35
% 1.83/1.35 thf(bl_says,definition,
% 1.83/1.35 ( bl_says
% 1.83/1.35 = ( ^ [K: individuals,A: $i > $o] : ( cs4_box @ ( cs4_impl @ ( bl_princ @ ( princ_inj @ K ) ) @ A ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(bl_valid_decl,type,
% 1.83/1.35 bl_valid: ( $i > $o ) > $o ).
% 1.83/1.35
% 1.83/1.35 thf(bl_valid_def,definition,
% 1.83/1.35 bl_valid = mvalid ).
% 1.83/1.35
% 1.83/1.35 thf(loca_decl,type,
% 1.83/1.35 loca: individuals ).
% 1.83/1.35
% 1.83/1.35 thf(loca_strength,axiom,
% 1.83/1.35 ( cs4_valid
% 1.83/1.35 @ ( cs4_all
% 1.83/1.35 @ ^ [K: individuals] : ( cs4_impl @ ( princ_inj @ K ) @ ( princ_inj @ loca ) ) ) ) ).
% 1.83/1.35
% 1.83/1.35 thf(spec,logic,
% 1.83/1.35 $$dhol ).
% 1.83/1.35
% 1.83/1.35 thf(bl_conceit,conjecture,
% 1.83/1.35 ! [K: individuals,A: $i > $o] : ( bl_valid @ ( bl_says @ K @ ( bl_impl @ ( bl_says @ K @ ( bl_atom @ A ) ) @ ( bl_atom @ A ) ) ) ) ).
% 1.83/1.35 ------------------------
% 1.83/1.37 % Exception at proof search level
% 1.83/1.37 Parsing Error on line 297
% 1.83/1.37 unit type, such as axiom or definition expected but logic found at position 162
%------------------------------------------------------------------------------