%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : LCL962^16 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/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 : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:35:17 AM UTC 2026
% Result : CounterSatisfiable 0.13s 0.45s
% Output : Saturation 0.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL962^16 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 21:14:39 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.38 ---- Original DTF file ---
% 0.13/0.38 thf(spec,logic,$$dhol).
% 0.13/0.38 %------------------------------------------------------------------------------
% 0.13/0.38 % File : LCL962^16 : TPTP v9.3.1. Released v8.1.0.
% 0.13/0.38 % Domain : Logic calculi
% 0.13/0.38 % Problem : Proving disprovability
% 0.13/0.38 % Version : [BP13] axioms.
% 0.13/0.38 % English : If A can prove that B can prove p whenever it is true, and
% 0.13/0.38 % if A can prove that B cannot prove p if that is true, and
% 0.13/0.38 % if p is not true, then A can prove that p is not true.
% 0.13/0.38
% 0.13/0.38 % Refs : [HA97] Huima & Aura (1997), Using Multimodal Logic to Express
% 0.13/0.38 % : [RO12] Raths & Otten (2012), The QMLTP Problem Library for Fi
% 0.13/0.38 % : [BP13] Benzmueller & Paulson (2013), Quantified Multimodal Lo
% 0.13/0.38 % : [Ste22] Steen (2022), An Extensible Logic Embedding Tool for L
% 0.13/0.38 % Source : [TPTP]
% 0.13/0.38 % Names : MML013+1 [QMLTP]
% 0.13/0.38
% 0.13/0.38 % Status : Theorem
% 0.13/0.38 % Rating : 0.08 v9.3.0, 0.11 v9.1.0, 0.12 v9.0.0, 0.10 v8.2.0, 0.23 v8.1.0
% 0.13/0.38 % Syntax : Number of formulae : 31 ( 10 unt; 15 typ; 8 def)
% 0.13/0.38 % Number of atoms : 48 ( 8 equ; 0 cnn)
% 0.13/0.39 % Maximal formula atoms : 9 ( 3 avg)
% 0.13/0.39 % Number of connectives : 77 ( 1 ~; 1 |; 4 &; 66 @)
% 0.13/0.39 % ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% 0.13/0.39 % Maximal formula depth : 9 ( 4 avg)
% 0.13/0.39 % Number of types : 3 ( 2 usr)
% 0.13/0.39 % Number of type conns : 49 ( 49 >; 0 *; 0 +; 0 <<)
% 0.13/0.39 % Number of symbols : 14 ( 13 usr; 3 con; 0-3 aty)
% 0.13/0.39 % Number of variables : 31 ( 21 ^; 9 !; 1 ?; 31 :)
% 0.13/0.39 % SPC : TH0_THM_EQU_NAR_NDT
% 0.13/0.39
% 0.13/0.39 % Comments : This output was generated by embedproblem, version 1.7.1 (library
% 0.13/0.39 % version 1.3). Generated on Thu Apr 28 13:18:18 EDT 2022 using
% 0.13/0.39 % 'modal' embedding, version 1.5.2. Logic specification used:
% 0.13/0.39 % $modal == [$constants == $rigid,$quantification == $cumulative,
% 0.13/0.39 % $modalities == $modal_system_S4].
% 0.13/0.39 %------------------------------------------------------------------------------
% 0.13/0.39 thf(mworld,type,
% 0.13/0.39 mworld: $tType ).
% 0.13/0.39
% 0.13/0.39 thf(mindex,type,
% 0.13/0.39 mindex: $tType ).
% 0.13/0.39
% 0.13/0.39 thf(mrel_type,type,
% 0.13/0.39 mrel: mindex > mworld > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf('#b_type',type,
% 0.13/0.39 '#b': mindex ).
% 0.13/0.39
% 0.13/0.39 thf('#a_type',type,
% 0.13/0.39 '#a': mindex ).
% 0.13/0.39
% 0.13/0.39 thf(mactual_type,type,
% 0.13/0.39 mactual: mworld ).
% 0.13/0.39
% 0.13/0.39 thf(mlocal_type,type,
% 0.13/0.39 mlocal: ( mworld > $o ) > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mlocal_def,definition,
% 0.13/0.39 ( mlocal
% 0.13/0.39 = ( ^ [Phi: mworld > $o] : ( Phi @ mactual ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mnot_type,type,
% 0.13/0.39 mnot: ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mand_type,type,
% 0.13/0.39 mand: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mor_type,type,
% 0.13/0.39 mor: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mimplies_type,type,
% 0.13/0.39 mimplies: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mequiv_type,type,
% 0.13/0.39 mequiv: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mnot_def,definition,
% 0.13/0.39 ( mnot
% 0.13/0.39 = ( ^ [A: mworld > $o,W: mworld] :
% 0.13/0.39 ~ ( A @ W ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mand_def,definition,
% 0.13/0.39 ( mand
% 0.13/0.39 = ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
% 0.13/0.39 ( ( A @ W )
% 0.13/0.39 & ( B @ W ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mor_def,definition,
% 0.13/0.39 ( mor
% 0.13/0.39 = ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
% 0.13/0.39 ( ( A @ W )
% 0.13/0.39 | ( B @ W ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mimplies_def,definition,
% 0.13/0.39 ( mimplies
% 0.13/0.39 = ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
% 0.13/0.39 ( ( A @ W )
% 0.13/0.39 => ( B @ W ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mequiv_def,definition,
% 0.13/0.39 ( mequiv
% 0.13/0.39 = ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
% 0.13/0.39 ( ( A @ W )
% 0.13/0.39 <=> ( B @ W ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mbox_type,type,
% 0.13/0.39 mbox: mindex > ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mbox_def,definition,
% 0.13/0.39 ( mbox
% 0.13/0.39 = ( ^ [R: mindex,Phi: mworld > $o,W: mworld] :
% 0.13/0.39 ! [V: mworld] :
% 0.13/0.39 ( ( mrel @ R @ W @ V )
% 0.13/0.39 => ( Phi @ V ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(mdia_type,type,
% 0.13/0.39 mdia: mindex > ( mworld > $o ) > mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(mdia_def,definition,
% 0.13/0.39 ( mdia
% 0.13/0.39 = ( ^ [R: mindex,Phi: mworld > $o,W: mworld] :
% 0.13/0.39 ? [V: mworld] :
% 0.13/0.39 ( ( mrel @ R @ W @ V )
% 0.13/0.39 & ( Phi @ V ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf('mrel_#b_reflexive',axiom,
% 0.13/0.39 ! [W: mworld] : ( mrel @ '#b' @ W @ W ) ).
% 0.13/0.39
% 0.13/0.39 thf('mrel_#b_transitive',axiom,
% 0.13/0.39 ! [W: mworld,V: mworld,U: mworld] :
% 0.13/0.39 ( ( ( mrel @ '#b' @ W @ V )
% 0.13/0.39 & ( mrel @ '#b' @ V @ U ) )
% 0.13/0.39 => ( mrel @ '#b' @ W @ U ) ) ).
% 0.13/0.39
% 0.13/0.39 thf('mrel_#a_reflexive',axiom,
% 0.13/0.39 ! [W: mworld] : ( mrel @ '#a' @ W @ W ) ).
% 0.13/0.39
% 0.13/0.39 thf('mrel_#a_transitive',axiom,
% 0.13/0.39 ! [W: mworld,V: mworld,U: mworld] :
% 0.13/0.39 ( ( ( mrel @ '#a' @ W @ V )
% 0.13/0.39 & ( mrel @ '#a' @ V @ U ) )
% 0.13/0.39 => ( mrel @ '#a' @ W @ U ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(p_decl,type,
% 0.13/0.39 p: mworld > $o ).
% 0.13/0.39
% 0.13/0.39 thf(ab_axiom_1,axiom,
% 0.13/0.39 mlocal @ ( mbox @ '#a' @ ( mimplies @ p @ ( mbox @ '#b' @ p ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(ab_axiom_2,axiom,
% 0.13/0.39 mlocal @ ( mimplies @ ( mnot @ ( mbox @ '#b' @ p ) ) @ ( mbox @ '#a' @ ( mnot @ ( mbox @ '#b' @ p ) ) ) ) ).
% 0.13/0.39
% 0.13/0.39 thf(not_a_axiom_1,axiom,
% 0.13/0.39 mlocal @ ( mnot @ p ) ).
% 0.13/0.39
% 0.13/0.39 thf(conj,conjecture,
% 0.13/0.39 mlocal @ ( mbox @ '#a' @ ( mnot @ p ) ) ).
% 0.13/0.39
% 0.13/0.39 %------------------------------------------------------------------------------
% 0.13/0.39 ------------------------
% 0.13/0.39 /starexec/sw/sutcliffe/jdk-11.0.2/bin/java: Command not found.
% 0.13/0.39 ---- Embedded in THF ---
% 0.13/0.39 ------------------------
% 0.13/0.41 ---- Cleaned THF ---
% 0.13/0.42 ------------------------
% 0.13/0.45 % (1045867)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_1045848 for (2999ds/2Mi)
% 0.13/0.45 % (1045867)First to succeed.
% 0.13/0.45 % SZS status Satisfiable for DTF2THF_1045848
% 0.13/0.45 % (1045867)# SZS output start Saturation.
% 0.13/0.45 % (1045867)# SZS output end Saturation.
% 0.13/0.45 % (1045867)------------------------------
% 0.13/0.45 % (1045867)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.13/0.45 % (1045867)Termination reason: Satisfiable
% 0.13/0.45
% 0.13/0.45 % (1045867)Memory used [KB]: 5373
% 0.13/0.45 % (1045867)Time elapsed: 0.002 s
% 0.13/0.45 % (1045867)Instructions burned: 1 (million)
% 0.13/0.45 % (1045867)------------------------------
% 0.13/0.45 % (1045867)------------------------------
% 0.13/0.45 % (1045863)Success in time 0.012 s
%------------------------------------------------------------------------------