TPTP Problem File: SWX180^1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX180^1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Benchmark: LCL698^1, Active target: mequiv
% Version : Especial.
% English :
% Refs : [Kon26] Kondylidou (2026), Email to Geoff Sutcliffe
% Source : [Kon26]
% Names : ALG444^1__005__axclos.verify [Kon26]
% Status : Theorem
% Rating : 0.42 v9.3.0
% Syntax : Number of formulae : 41 ( 1 unt; 39 typ; 0 def)
% Number of atoms : 76 ( 41 equ; 0 cnn)
% Maximal formula atoms : 39 ( 38 avg)
% Number of connectives : 229 ( 52 ~; 30 |; 36 &; 109 @)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 21 avg)
% Number of types : 6 ( 4 usr)
% Number of type conns : 172 ( 172 >; 0 *; 0 +; 0 <<)
% Number of symbols : 36 ( 35 usr; 2 con; 0-3 aty)
% Number of variables : 100 ( 53 ^; 45 !; 2 ?; 100 :)
% SPC : TH0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
thf(unsorted_type,type,
unsorted: $tType ).
thf(mu_type,type,
mu: $tType ).
thf(meq_ind_decl,type,
meq_ind: mu > mu > $i > $o ).
thf(meq_prop_decl,type,
meq_prop: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mnot_decl,type,
mnot: ( $i > $o ) > $i > $o ).
thf(mor_decl,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mand_decl,type,
mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mimplies_decl,type,
mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mimplied_decl,type,
mimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mequiv_decl,type,
mequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mxor_decl,type,
mxor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mforall_ind_decl,type,
mforall_ind: ( mu > $i > $o ) > $i > $o ).
thf(mforall_prop_decl,type,
mforall_prop: ( ( $i > $o ) > $i > $o ) > $i > $o ).
thf(mexists_ind_decl,type,
mexists_ind: ( mu > $i > $o ) > $i > $o ).
thf(mexists_prop_decl,type,
mexists_prop: ( ( $i > $o ) > $i > $o ) > $i > $o ).
thf(mtrue_decl,type,
mtrue: $i > $o ).
thf(mfalse_decl,type,
mfalse: $i > $o ).
thf(mbox_decl,type,
mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mdia_decl,type,
mdia: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(mreflexive_decl,type,
mreflexive: ( $i > $i > $o ) > $o ).
thf(msymmetric_decl,type,
msymmetric: ( $i > $i > $o ) > $o ).
thf(mserial_decl,type,
mserial: ( $i > $i > $o ) > $o ).
thf(mtransitive_decl,type,
mtransitive: ( $i > $i > $o ) > $o ).
thf(meuclidean_decl,type,
meuclidean: ( $i > $i > $o ) > $o ).
thf(mpartially_functional_decl,type,
mpartially_functional: ( $i > $i > $o ) > $o ).
thf(mfunctional_decl,type,
mfunctional: ( $i > $i > $o ) > $o ).
thf(mweakly_dense_decl,type,
mweakly_dense: ( $i > $i > $o ) > $o ).
thf(mweakly_connected_decl,type,
mweakly_connected: ( $i > $i > $o ) > $o ).
thf(mweakly_directed_decl,type,
mweakly_directed: ( $i > $i > $o ) > $o ).
thf(mvalid_decl,type,
mvalid: ( $i > $o ) > $o ).
thf(minvalid_decl,type,
minvalid: ( $i > $o ) > $o ).
thf(msatisfiable_decl,type,
msatisfiable: ( $i > $o ) > $o ).
thf(mcountersatisfiable_decl,type,
mcountersatisfiable: ( $i > $o ) > $o ).
%----Types of the domains
thf(d_unsorted_type,type,
d_unsorted: $tType ).
thf(d_mu_type,type,
d_mu: $tType ).
%----Types of the promotion functions
thf(d2unsorted_decl,type,
d2unsorted: d_unsorted > $i ).
thf(d2mu_decl,type,
d2mu: d_mu > mu ).
%----Types of the domain elements
thf(d_unsorted_0_decl,type,
d_unsorted_0: d_unsorted ).
thf(d_mu_0_decl,type,
d_mu_0: d_mu ).
thf(lcl698_1,axiom,
( ! [U: $i] :
? [DU: d_unsorted] :
( U
= ( d2unsorted @ DU ) )
& ! [DU: d_unsorted] : ( DU = d_unsorted_0 )
& ! [DU1: d_unsorted,DU2: d_unsorted] :
( ( ( d2unsorted @ DU1 )
= ( d2unsorted @ DU2 ) )
=> ( DU1 = DU2 ) )
& ! [M: mu] :
? [DM: d_mu] :
( M
= ( d2mu @ DM ) )
& ! [DM: d_mu] : ( DM = d_mu_0 )
& ! [DM1: d_mu,DM2: d_mu] :
( ( ( d2mu @ DM1 )
= ( d2mu @ DM2 ) )
=> ( DM1 = DM2 ) )
& ( meq_prop
= ( ^ [X: $i > $o,Y: $i > $o,W: $i] :
( ( X @ W )
= ( Y @ W ) ) ) )
& ( mnot
= ( ^ [Phi: $i > $o,W: $i] :
~ ( Phi @ W ) ) )
& ( mor
= ( ^ [Phi: $i > $o,Psi: $i > $o,W: $i] :
( ( Phi @ W )
| ( Psi @ W ) ) ) )
& ( mand
= ( ^ [Phi: $i > $o,Psi: $i > $o,Flatten_var_0: $i] :
~ ( ~ ( Phi @ Flatten_var_0 )
| ~ ( Psi @ Flatten_var_0 ) ) ) )
& ( mimplies
= ( ^ [Phi: $i > $o,Psi: $i > $o,Flatten_var_0: $i] :
( ~ ( Phi @ Flatten_var_0 )
| ( Psi @ Flatten_var_0 ) ) ) )
& ( mimplied
= ( ^ [Phi: $i > $o,Psi: $i > $o,Flatten_var_0: $i] :
( ~ ( Psi @ Flatten_var_0 )
| ( Phi @ Flatten_var_0 ) ) ) )
& ( mequiv
= ( ^ [Phi: $i > $o,Psi: $i > $o,Flatten_var_0: $i] :
~ ( ~ ( ~ ( Phi @ Flatten_var_0 )
| ( Psi @ Flatten_var_0 ) )
| ~ ( ~ ( Psi @ Flatten_var_0 )
| ( Phi @ Flatten_var_0 ) ) ) ) )
& ( mxor
= ( ^ [Phi: $i > $o,Psi: $i > $o,Flatten_var_0: $i] :
( ~ ( ~ ( Phi @ Flatten_var_0 )
| ( Psi @ Flatten_var_0 ) )
| ~ ( ~ ( Psi @ Flatten_var_0 )
| ( Phi @ Flatten_var_0 ) ) ) ) )
& ( mforall_ind
= ( ^ [Phi: mu > $i > $o,W: $i] :
! [X: mu] : ( Phi @ X @ W ) ) )
& ( mforall_prop
= ( ^ [Phi: ( $i > $o ) > $i > $o,W: $i] :
! [P: $i > $o] : ( Phi @ P @ W ) ) )
& ( mexists_ind
= ( ^ [Phi: mu > $i > $o,Flatten_var_0: $i] :
~ ! [X: mu] :
~ ( Phi @ X @ Flatten_var_0 ) ) )
& ( mexists_prop
= ( ^ [Phi: ( $i > $o ) > $i > $o,Flatten_var_0: $i] :
~ ! [P: $i > $o] :
~ ( Phi @ P @ Flatten_var_0 ) ) )
& ( mbox
= ( ^ [R: $i > $i > $o,Phi: $i > $o,W: $i] :
! [V: $i] :
( ~ ( R @ W @ V )
| ( Phi @ V ) ) ) )
& ( mdia
= ( ^ [R: $i > $i > $o,Phi: $i > $o,Flatten_var_0: $i] :
~ ! [V: $i] :
( ~ ( R @ Flatten_var_0 @ V )
| ~ ( Phi @ V ) ) ) )
& ( mreflexive
= ( ^ [R: $i > $i > $o] :
! [S: $i] : ( R @ S @ S ) ) )
& ( msymmetric
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i] :
( ~ ( R @ S @ T )
| ( R @ T @ S ) ) ) )
& ( mserial
= ( ^ [R: $i > $i > $o] :
! [S: $i] :
~ ! [T: $i] :
~ ( R @ S @ T ) ) )
& ( mtransitive
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i,U: $i] :
( ~ ( R @ S @ T )
| ~ ( R @ T @ U )
| ( R @ S @ U ) ) ) )
& ( meuclidean
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i,U: $i] :
( ~ ( R @ S @ T )
| ~ ( R @ S @ U )
| ( R @ T @ U ) ) ) )
& ( mpartially_functional
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i,U: $i] :
( ~ ( R @ S @ T )
| ~ ( R @ S @ U )
| ( T = U ) ) ) )
& ( mfunctional
= ( ^ [R: $i > $i > $o] :
! [S: $i] :
~ ! [T: $i] :
( ~ ( R @ S @ T )
| ~ ! [U: $i] :
( ~ ( R @ S @ U )
| ( T = U ) ) ) ) )
& ( mweakly_dense
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i] :
( ~ ( R @ S @ T )
| ~ ! [Bound_variable_953: $i] :
( ~ ( R @ S @ Bound_variable_953 )
| ~ ( R @ Bound_variable_953 @ T ) ) ) ) )
& ( mweakly_connected
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i,U: $i] :
( ~ ( R @ S @ T )
| ~ ( R @ S @ U )
| ( R @ T @ U )
| ( T = U )
| ( R @ U @ T ) ) ) )
& ( mweakly_directed
= ( ^ [R: $i > $i > $o] :
! [S: $i,T: $i,U: $i] :
( ~ ( R @ S @ T )
| ~ ( R @ S @ U )
| ~ ! [V: $i] :
( ~ ( R @ T @ V )
| ~ ( R @ U @ V ) ) ) ) )
& ( mvalid
= ( ^ [Phi: $i > $o] :
! [W: $i] : ( Phi @ W ) ) )
& ( minvalid
= ( ^ [Phi: $i > $o] :
! [W: $i] :
~ ( Phi @ W ) ) )
& ( msatisfiable
= ( ^ [Phi: $i > $o] :
~ ! [W: $i] :
~ ( Phi @ W ) ) )
& ( mcountersatisfiable
= ( ^ [Phi: $i > $o] :
~ ! [W: $i] : ( Phi @ W ) ) )
& ( meq_ind @ ( d2mu @ d_mu_0 ) @ ( d2mu @ d_mu_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
& ( mtrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( mfalse @ ( d2unsorted @ d_unsorted_0 ) ) ) ).
thf(mequiv,conjecture,
( mequiv
= ( ^ [Phi: $i > $o,Psi: $i > $o] : ( mand @ ( mimplies @ Phi @ Psi ) @ ( mimplies @ Psi @ Phi ) ) ) ) ).
%------------------------------------------------------------------------------