TPTP Problem File: SWX152_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX152_1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Bounded synthesis
% Version : Especial.
% English :
% Refs : [SF07] Schewe & Finkbeiner (2007), Bounded Synthesis
% : [Kru09] Kruglov (2009), Email to Geoff Sutcliffe
% Source : [Kru09]
% Names : afm07_2.dfg [Kru09]
% Status : Satisfiable
% Rating : 0.67 v9.3.0
% Syntax : Number of formulae : 36 ( 0 unt; 24 typ; 0 def)
% Number of atoms : 79 ( 20 equ)
% Maximal formula atoms : 10 ( 6 avg)
% Number of connectives : 77 ( 10 ~; 3 |; 58 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number arithmetic : 42 ( 20 atm; 0 fun; 11 num; 11 var)
% Number of types : 2 ( 0 usr; 1 ari)
% Number of type conns : 28 ( 24 >; 4 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 0 prp; 1-2 aty)
% Number of functors : 19 ( 17 usr; 2 con; 0-2 aty)
% Number of variables : 11 ( 11 !; 0 ?; 11 :)
% SPC : TF0_SAT_EQU_ARI
% Comments :
%------------------------------------------------------------------------------
tff(type_tau00,type,
tau00: $int > $int ).
tff(type_tau01,type,
tau01: $int > $int ).
tff(type_tau10,type,
tau10: $int > $int ).
tff(type_tau11,type,
tau11: $int > $int ).
tff(type_lambdaI1,type,
lambdai1: $int > $int ).
tff(type_lambdaI2,type,
lambdai2: $int > $int ).
tff(type_lambdaI3,type,
lambdai3: $int > $int ).
tff(type_lambdaI4,type,
lambdai4: $int > $int ).
tff(type_lambdaI5,type,
lambdai5: $int > $int ).
tff(type_d1,type,
d1: $int > $int ).
tff(type_d2,type,
d2: $int > $int ).
tff(type_g1,type,
g1: $int > $int ).
tff(type_g2,type,
g2: $int > $int ).
tff(type_tauR11,type,
taur11: ( $int * $int ) > $int ).
tff(type_tauR1b1,type,
taur1b1: ( $int * $int ) > $int ).
tff(type_tauR22,type,
taur22: ( $int * $int ) > $int ).
tff(type_tauR2b2,type,
taur2b2: ( $int * $int ) > $int ).
tff(type_lambdaB1,type,
lambdab1: $int > $o ).
tff(type_lambdaB2,type,
lambdab2: $int > $o ).
tff(type_lambdaB3,type,
lambdab3: $int > $o ).
tff(type_lambdaB4,type,
lambdab4: $int > $o ).
tff(type_lambdaB5,type,
lambdab5: $int > $o ).
tff(type_r1,type,
r1: $int > $o ).
tff(type_r2,type,
r2: $int > $o ).
%----g1(x) and g2(x) are boolean-like (0 or 1)
tff(ax1,axiom,
! [X: $int] :
( ( g1(X) = 0 )
| ( g1(X) = 1 ) ) ).
tff(ax2,axiom,
! [X: $int] :
( ( g2(X) = 0 )
| ( g2(X) = 1 ) ) ).
%----R1/R2 combinations on tau functions
tff(ax3,axiom,
! [X: $int] :
( r1(tau11(X))
& r2(tau11(X))
& r1(tau10(X))
& ~ r2(tau10(X))
& ~ r1(tau01(X))
& r2(tau01(X))
& ~ r1(tau00(X))
& ~ r2(tau00(X)) ) ).
%----LambdaB1(0) base condition
tff(ax4,axiom,
( lambdab1(0)
& ~ r1(0)
& ~ r2(0) ) ).
%----LambdaB1 closure properties
tff(ax5,axiom,
! [X: $int] :
( lambdab1(X)
=> ( lambdab1(tau00(X))
& $greatereq(lambdai1(tau00(X)),lambdai1(X))
& lambdab1(tau01(X))
& $greatereq(lambdai1(tau01(X)),lambdai1(X))
& lambdab1(tau10(X))
& $greatereq(lambdai1(tau10(X)),lambdai1(X))
& lambdab1(tau11(X))
& $greatereq(lambdai1(tau11(X)),lambdai1(X)) ) ) ).
%----LambdaB1 => not(g1(d1(x))=1 and g2(d2(x))=1)
tff(ax6,axiom,
! [X: $int] :
( lambdab1(X)
=> ( ( g1(d1(X)) != 1 )
| ( g2(d2(X)) != 1 ) ) ) ).
%----LambdaB1 & R1 => LambdaB2 propagation
tff(ax7,axiom,
! [X: $int] :
( ( lambdab1(X)
& r1(X) )
=> ( lambdab2(tau00(X))
& $greatereq(lambdai2(tau00(X)),lambdai1(X))
& lambdab2(tau01(X))
& $greatereq(lambdai2(tau01(X)),lambdai1(X))
& lambdab2(tau10(X))
& $greatereq(lambdai2(tau10(X)),lambdai1(X))
& lambdab2(tau11(X))
& $greatereq(lambdai2(tau11(X)),lambdai1(X)) ) ) ).
%----LambdaB1 & R2 => LambdaB3 propagation
tff(ax8,axiom,
! [X: $int] :
( ( lambdab1(X)
& r2(X) )
=> ( lambdab3(tau00(X))
& $greatereq(lambdai3(tau00(X)),lambdai1(X))
& lambdab3(tau01(X))
& $greatereq(lambdai3(tau01(X)),lambdai1(X))
& lambdab3(tau10(X))
& $greatereq(lambdai3(tau10(X)),lambdai1(X))
& lambdab3(tau11(X))
& $greatereq(lambdai3(tau11(X)),lambdai1(X)) ) ) ).
%----LambdaB2 & not(g1(d2(x))=1) => LambdaB2 propagation
tff(ax9,axiom,
! [X: $int] :
( ( lambdab2(X)
& ( g1(d2(X)) != 1 ) )
=> ( lambdab2(tau00(X))
& $greatereq(lambdai2(tau00(X)),lambdai2(X))
& lambdab2(tau01(X))
& $greatereq(lambdai2(tau01(X)),lambdai2(X))
& lambdab2(tau10(X))
& $greatereq(lambdai2(tau10(X)),lambdai2(X))
& lambdab2(tau11(X))
& $greatereq(lambdai2(tau11(X)),lambdai2(X)) ) ) ).
%----LambdaB3 & not(g2(d2(x))=1) => LambdaB3 propagation
tff(ax10,axiom,
! [X: $int] :
( ( lambdab3(X)
& ( g2(d2(X)) != 1 ) )
=> ( lambdab3(tau00(X))
& $greatereq(lambdai3(tau00(X)),lambdai3(X))
& lambdab3(tau01(X))
& $greatereq(lambdai3(tau01(X)),lambdai3(X))
& lambdab3(tau10(X))
& $greatereq(lambdai3(tau10(X)),lambdai3(X))
& lambdab3(tau11(X))
& $greatereq(lambdai3(tau11(X)),lambdai3(X)) ) ) ).
%----TauR11 / TauR1b1 and d1 consistency
tff(ax11,axiom,
! [X: $int] :
( ( taur11(g2(d2(X)),d1(X)) = d1(tau11(X)) )
& ( taur11(g2(d2(X)),d1(X)) = d1(tau10(X)) )
& ( d1(tau11(X)) = d1(tau10(X)) )
& ( taur1b1(g2(d2(X)),d1(X)) = d1(tau01(X)) )
& ( taur1b1(g2(d2(X)),d1(X)) = d1(tau00(X)) )
& ( d1(tau01(X)) = d1(tau00(X)) ) ) ).
%----TauR22 / TauR2b2 and d2 consistency
tff(ax12,axiom,
! [X: $int] :
( ( taur22(g1(d1(X)),d2(X)) = d2(tau11(X)) )
& ( taur22(g1(d1(X)),d2(X)) = d2(tau01(X)) )
& ( d2(tau11(X)) = d2(tau01(X)) )
& ( taur2b2(g1(d1(X)),d2(X)) = d2(tau10(X)) )
& ( taur2b2(g1(d1(X)),d2(X)) = d2(tau00(X)) )
& ( d2(tau10(X)) = d2(tau00(X)) ) ) ).
%------------------------------------------------------------------------------