TPTP Problem File: SWX176^1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX176^1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Benchmark: LCL696^1, Active target: ior
% 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 : 26 ( 1 unt; 24 typ; 0 def)
% Number of atoms : 69 ( 22 equ; 0 cnn)
% Maximal formula atoms : 24 ( 34 avg)
% Number of connectives : 188 ( 38 ~; 32 |; 26 &; 91 @)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 14 avg)
% Number of types : 4 ( 2 usr)
% Number of type conns : 98 ( 98 >; 0 *; 0 +; 0 <<)
% Number of symbols : 23 ( 22 usr; 1 con; 0-3 aty)
% Number of variables : 73 ( 41 ^; 31 !; 1 ?; 73 :)
% SPC : TH0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
thf(unsorted_type,type,
unsorted: $tType ).
thf(irel_decl,type,
irel: $i > $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(mbox_s4_decl,type,
mbox_s4: ( $i > $o ) > $i > $o ).
thf(iatom_decl,type,
iatom: ( $i > $o ) > $i > $o ).
thf(inot_decl,type,
inot: ( $i > $o ) > $i > $o ).
thf(itrue_decl,type,
itrue: $i > $o ).
thf(ifalse_decl,type,
ifalse: $i > $o ).
thf(iand_decl,type,
iand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(ior_decl,type,
ior: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(iimplies_decl,type,
iimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(iimplied_decl,type,
iimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(iequiv_decl,type,
iequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(ixor_decl,type,
ixor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(ivalid_decl,type,
ivalid: ( $i > $o ) > $o ).
thf(isatisfiable_decl,type,
isatisfiable: ( $i > $o ) > $o ).
thf(icountersatisfiable_decl,type,
icountersatisfiable: ( $i > $o ) > $o ).
thf(iinvalid_decl,type,
iinvalid: ( $i > $o ) > $o ).
%----Types of the domains
thf(d_unsorted_type,type,
d_unsorted: $tType ).
%----Types of the promotion functions
thf(d2unsorted_decl,type,
d2unsorted: d_unsorted > $i ).
%----Types of the domain elements
thf(d_unsorted_0_decl,type,
d_unsorted_0: d_unsorted ).
thf(lcl696_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 ) )
& ( mnot
= ( ^ [X: $i > $o,U: $i] :
~ ( X @ U ) ) )
& ( mor
= ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
( ( X @ U )
| ( Y @ U ) ) ) )
& ( mand
= ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
( ( X @ U )
& ( Y @ U ) ) ) )
& ( mimplies
= ( ^ [U: $i > $o,V: $i > $o,Flatten_var_0: $i] :
( ~ ( U @ Flatten_var_0 )
| ( V @ Flatten_var_0 ) ) ) )
& ( mbox_s4
= ( ^ [P: $i > $o,X: $i] :
! [Y: $i] :
( ~ ( irel @ X @ Y )
| ( P @ Y ) ) ) )
& ( iatom
= ( ^ [P: $i > $o,Flatten_var_0: $i] : ( P @ Flatten_var_0 ) ) )
& ( inot
= ( ^ [P: $i > $o,Flatten_var_0: $i] :
~ ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( P @ Y ) ) ) )
& ( iand
= ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
( ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( P @ Y ) )
& ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( Q @ Y ) ) ) ) )
& ( ior
= ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
( ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( P @ Y ) )
| ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( Q @ Y ) ) ) ) )
& ( iimplies
= ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
( ~ ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( P @ Y ) )
| ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( Q @ Y ) ) ) ) )
& ( iimplied
= ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
( ~ ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( Q @ Y ) )
| ! [Y: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( P @ Y ) ) ) ) )
& ( iequiv
= ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
( ! [Y: $i,Bound_variable_718: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ~ ! [Bound_variable_693: $i] :
( ~ ( irel @ Y @ Bound_variable_693 )
| ( P @ Bound_variable_693 ) )
| ~ ( irel @ Y @ Bound_variable_718 )
| ( Q @ Bound_variable_718 ) )
& ! [Y: $i,Bound_variable_771: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ~ ! [Bound_variable_746: $i] :
( ~ ( irel @ Y @ Bound_variable_746 )
| ( Q @ Bound_variable_746 ) )
| ~ ( irel @ Y @ Bound_variable_771 )
| ( P @ Bound_variable_771 ) ) ) ) )
& ( ixor
= ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
~ ! [Y: $i,Bound_variable_849: $i,Bound_variable_851: $i,Bound_variable_864: $i,Bound_variable_866: $i] :
( ~ ( irel @ Flatten_var_0 @ Y )
| ( ( ~ ( irel @ Y @ Bound_variable_849 )
| ~ ! [Bound_variable_693: $i] :
( ~ ( irel @ Bound_variable_849 @ Bound_variable_693 )
| ( P @ Bound_variable_693 ) )
| ~ ( irel @ Bound_variable_849 @ Bound_variable_851 )
| ( Q @ Bound_variable_851 ) )
& ( ~ ( irel @ Y @ Bound_variable_864 )
| ~ ! [Bound_variable_746: $i] :
( ~ ( irel @ Bound_variable_864 @ Bound_variable_746 )
| ( Q @ Bound_variable_746 ) )
| ~ ( irel @ Bound_variable_864 @ Bound_variable_866 )
| ( P @ Bound_variable_866 ) ) ) ) ) )
& ( ivalid
= ( ^ [Phi: $i > $o] :
! [W: $i] : ( Phi @ W ) ) )
& ( isatisfiable
= ( ^ [Phi: $i > $o] :
~ ! [W: $i] :
~ ( Phi @ W ) ) )
& ( icountersatisfiable
= ( ^ [Phi: $i > $o] :
~ ! [W: $i] : ( Phi @ W ) ) )
& ( iinvalid
= ( ^ [Phi: $i > $o] :
! [W: $i] :
~ ( Phi @ W ) ) )
& ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
& ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( ifalse @ ( d2unsorted @ d_unsorted_0 ) ) ) ).
thf(ior,conjecture,
( ior
= ( ^ [P: $i > $o,Q: $i > $o] : ( mor @ ( mbox_s4 @ P ) @ ( mbox_s4 @ Q ) ) ) ) ).
%------------------------------------------------------------------------------