1 files changed, 100 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/SYO056^1.p b/test/regress/regress1/ho/SYO056^1.p
new file mode 100644
index 000000000..a8a6bafca
--- /dev/null
+++ b/test/regress/regress1/ho/SYO056^1.p
@@ -0,0 +1,100 @@
+% COMMAND-LINE:  --uf-ho --finite-model-find
+% EXPECT: % SZS status CounterSatisfiable for SYO056^1
+
+%------------------------------------------------------------------------------
+% File     : SYO056^1 : TPTP v7.2.0. Released v4.0.0.
+% Domain   : Logic Calculi (Quantified multimodal logic)
+% Problem  : Simple textbook example 13
+% Version  : [Ben09] axioms.
+% English  :
+
+% Refs     : [Gol92] Goldblatt (1992), Logics of Time and Computation
+%          : [Ben09] Benzmueller (2009), Email to Geoff Sutcliffe
+% Source   : [Ben09]
+% Names    : ex13.p [Ben09]
+
+% Status   : CounterSatisfiable
+% Rating   : 0.25 v7.2.0, 0.33 v6.4.0, 0.00 v6.3.0, 0.33 v5.4.0, 0.00 v5.0.0, 0.67 v4.1.0, 0.50 v4.0.0
+% Syntax   : Number of formulae    :   64 (   0 unit;  32 type;  31 defn)
+%            Number of atoms       :  238 (  36 equality; 137 variable)
+%            Maximal formula depth :   12 (   6 average)
+%            Number of connectives :  138 (   4   ~;   4   |;   8   &; 114   @)
+%                                         (   0 <=>;   8  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :  172 ( 172   >;   0   *;   0   +;   0  <<)
+%            Number of symbols     :   36 (  32   :;   0   =)
+%            Number of variables   :   87 (   3 sgn;  30   !;   6   ?;  51   ^)
+%                                         (  87   :;   0  !>;   0  ?*)
+%                                         (   0  @-;   0  @+)
+% SPC      : TH0_CSA_EQU_NAR
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Include embedding of quantified multimodal logic in simple type theory
+%% include('Axioms/LCL013^0.ax').
+%------------------------------------------------------------------------------
+thf(mvalid_type,type,(
+    mvalid: ( $i > $o ) > $o )).
+
+thf(mvalid,definition,
+    ( mvalid
+    = ( ^ [Phi: $i > $o] :
+        ! [W: $i] :
+          ( Phi @ W ) ) )).
+
+
+thf(mforall_prop_type,type,(
+    mforall_prop: ( ( $i > $o ) > $i > $o ) > $i > $o )).
+
+thf(mforall_prop,definition,
+    ( mforall_prop
+    = ( ^ [Phi: ( $i > $o ) > $i > $o,W: $i] :
+        ! [P: $i > $o] :
+          ( Phi @ P @ W ) ) )).
+
+thf(mnot_type,type,(
+    mnot: ( $i > $o ) > $i > $o )).
+
+thf(mnot,definition,
+    ( mnot
+    = ( ^ [Phi: $i > $o,W: $i] :
+          ~ ( Phi @ W ) ) )).
+
+thf(mor_type,type,(
+    mor: ( $i > $o ) > ( $i > $o ) > $i > $o )).
+
+thf(mor,definition,
+    ( mor
+    = ( ^ [Phi: $i > $o,Psi: $i > $o,W: $i] :
+          ( ( Phi @ W )
+          | ( Psi @ W ) ) ) )).
+
+thf(mimplies_type,type,(
+    mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o )).
+
+thf(mimplies,definition,
+    ( mimplies
+    = ( ^ [Phi: $i > $o,Psi: $i > $o] :
+          ( mor @ ( mnot @ Phi ) @ Psi ) ) )).
+
+thf(mbox_type,type,(
+    mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o )).
+
+thf(mbox,definition,
+    ( mbox
+    = ( ^ [R: $i > $i > $o,Phi: $i > $o,W: $i] :
+        ! [V: $i] :
+          ( ~ ( R @ W @ V )
+          | ( Phi @ V ) ) ) )).
+
+
+thf(conj,conjecture,(
+    ! [R: $i > $i > $o] :
+      ( mvalid
+      @ ( mforall_prop
+        @ ^ [A: $i > $o] :
+            ( mforall_prop
+            @ ^ [B: $i > $o] :
+                ( mimplies @ ( mbox @ R @ ( mor @ A @ B ) ) @ ( mor @ ( mbox @ R @ A ) @ ( mbox @ R @ B ) ) ) ) ) ) )).
+
+%------------------------------------------------------------------------------