awk% bobj
                     \|||||||||||||||||/
                   --- Welcome to BOBJ ---
                     /|||||||||||||||||\
      BOBJ version 0.9.197 built: Tue Nov  5 12:12:21 PST 2002
               University of California, San Diego
                  Wed Nov 06 10:49:14 PST 2002
BOBJ> in pete
==========================================
bth STREAM
==========================================
***>  fair boolean stream (no infinite consecutive true or false)
==========================================
bth FAIR-STREAM
==========================================
dth MACHINE
Warning: redefining module MACHINE
==========================================
dth SYSTEM-STATE
Warning: redefining module SYSTEM-STATE
==========================================
bth PETERSON
==========================================
dth PROOF
==========================================
cases C1
==========================================
cases C2
==========================================
cases C3
==========================================
cases C4
==========================================
cases C5
==========================================
cases C6
==========================================
cases C7
==========================================
cases C8
==========================================
cases C9
==========================================
cases C10
==========================================
***>   mutual exclusion property
==========================================
open PROOF
==========================================
use C1 * C2 * C3 * C4 * C5 * C6 * C7 * C8 * C9 * C10
==========================================
var F : Flag
==========================================
vars M N : Nat
==========================================
vars Ba Bb Da Db : Bool
==========================================
vars Ra Rb : Request
==========================================
var Fs : FairStream
==========================================
set cobasis COB
==========================================
c-reduce in PROOF : sys ([(F | (< Ba , Da , M >) | (< Bb , Db , N >)) 
    , Ra , Rb , Fs]) == all-true if good (F | (< Ba , Da , M >) | (< 
    Bb , Db , N >)) 
using cobasis COB for PROOF
-------------------------------------------
case analysis by C1 * C2 * C3 * C4 * C5 * C6 * C7 * C8 * C9 * C10
-------------------------------------------
introduce constant(s): 
    r for the variable Ra
    f1 for the variable Fs
    r1 for the variable Rb
-------------------------------
case (1,1,1,1,1,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,1,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,1,2,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,1,2,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,1,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,1,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,1,2,2,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,1,2,2,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = true 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,1,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,1,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,1,2,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , 0 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , 0 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , n 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , n 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< false , false , 0 >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        0 >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        0 >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        0 >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        n >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        n >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< false , false , 
        n >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,1,2,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = true 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , (p m) >) | (< true , false , 
        (hd r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,1,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,1,2,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = true 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
the condition is false: good (f | (< ba , da , m >) | (< bb , 
    db , n >)) 
-------------------------------
case (1,1,2,2,2,1,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< false , false , 0 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< false , false , 0 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< false , false , n 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< false , false , n 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , 0 >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,1,2,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m = 0 
        n > 0 = true 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , 0 >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< false , false , 0 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< false , false , 0 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,2,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = true 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , 0 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,1,2,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n = 0 
        (hd r) > 0 = true 
        (hd r1) > 0 = true 
        fhd f1 = false 
        true = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,2,1,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,2,1,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< false , false , n 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,2,1,2,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,2,1,2,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        hd r = 0 
        (hd r1) > 0 = true 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< true , false , (hd 
        r1) >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,2,2,1,1) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = true 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , true , m >) | (< false , false , n 
        >)) , r , r1 , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
    r1 , f1])) == all-true 
    nf: true
-------------------------------
case (1,1,2,2,2,2,2,2,1,2) : 
assume: f = a 
        ba = true 
        bb = false 
        da = false 
        db = false 
        m > 0 = true 
        n > 0 = true 
        (hd r) > 0 = true 
        hd r1 = 0 
        fhd f1 = false 
        eq(n, 0) = true
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >)) , r , 
        r1 , f1])) == all-true 
    nf: sys ([(a | (< true , false , m >) | (< false , false , n 
        >)) , r , (tl r1) , (ftl f1)]) == all-true 
-------------------------------
deduce to : all-true == all-true 
reduce: sys (tl ([(f | (< ba , da , m >) | (< bb , db , n >))