The bear is rough. All red, young things are nice. If the bear is nice and the bear is red then the bear is young. All rough, red things are young. Rough things are nice. If something is kind then it is red. Kind things are nice. If the bear is nice then the bear is kind. If the bear is nice and the bear is red then the bear is rough.
The bear is rough.
("bear" "is" "rough" "+")
All red, young things are nice.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If the bear is nice and the bear is red then the bear is young.
((("bear" "is" "nice" "+") ("bear" "is" "red" "+")) -> ("bear" "is" "young" "+"))
All rough, red things are young.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If the bear is nice then the bear is kind.
((("bear" "is" "nice" "+")) -> ("bear" "is" "kind" "+"))
If the bear is nice and the bear is red then the bear is rough.
((("bear" "is" "nice" "+") ("bear" "is" "red" "+")) -> ("bear" "is" "rough" "+"))
The bear is rough.
True
1
proof
[(triple1)]
("bear" "is" "rough" "+")
triple1
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The bear is nice.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "nice" "-")
((triple1) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("bear" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("bear" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is red.
True
4
proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule5))]
("bear" "is" "red" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is not red.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule5))]
("bear" "is" "red" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is rough.[(triple1)] @1: The bear is nice.[(((triple1) -> rule4))] @2: The bear is kind.[(((((triple1) -> rule4)) -> rule7))] @3: The bear is red.[(((((((triple1) -> rule4)) -> rule7)) -> rule5))] @4: The bear is young.[(((triple1 ((((((triple1) -> rule4)) -> rule7)) -> rule5)) -> rule3) OR ((((triple1) -> rule4) ((((((triple1) -> rule4)) -> rule7)) -> rule5)) -> rule2))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is young.
("bear" "is" "young" "+")
((triple1 ((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4