The bear is kind. The bear is red. The bear is young. Nice things are young. Rough things are red. All kind, rough things are nice. If something is kind and young then it is nice. If the bear is rough then the bear is young. Young, red things are kind. Rough things are young. If the bear is young and the bear is nice then the bear is rough.
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All kind, rough things are nice.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is kind and young then it is nice.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If the bear is rough then the bear is young.
((("bear" "is" "rough" "+")) -> ("bear" "is" "young" "+"))
Young, red things are kind.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If the bear is young and the bear is nice then the bear is rough.
((("bear" "is" "young" "+") ("bear" "is" "nice" "+")) -> ("bear" "is" "rough" "+"))
The bear is kind.
True
1
proof
[(triple1 OR ((triple3 triple2) -> rule6))]
("bear" "is" "kind" "+")
triple1
((triple3 triple2) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not kind.
False
1
inv-proof
[(triple1 OR ((triple3 triple2) -> rule6))]
("bear" "is" "kind" "-")
triple1
((triple3 triple2) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
True
3
proof
[(((triple1 triple3) -> rule4) OR ((((triple3 triple2) -> rule6) triple3) -> rule4))]
("bear" "is" "nice" "+")
((triple1 triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is not nice.
False
3
inv-proof
[(((triple1 triple3) -> rule4) OR ((((triple3 triple2) -> rule6) triple3) -> rule4))]
("bear" "is" "nice" "-")
((triple1 triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is rough.
True
5
proof
[(((triple3 ((triple1 triple3) -> rule4)) -> rule8) OR ((triple3 ((((triple3 triple2) -> rule6) triple3) -> rule4)) -> rule8))]
("bear" "is" "rough" "+")
((triple3 ((triple1 triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((triple3 ((((triple3 triple2) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear is not rough.
False
5
inv-proof
[(((triple3 ((triple1 triple3) -> rule4)) -> rule8) OR ((triple3 ((((triple3 triple2) -> rule6) triple3) -> rule4)) -> rule8))]
("bear" "is" "rough" "-")
((triple3 ((triple1 triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((triple3 ((((triple3 triple2) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "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 kind.[(triple1 OR ((triple3 triple2) -> rule6))] The bear is red.[(triple2 OR ((((triple3 ((triple1 triple3) -> rule4)) -> rule8)) -> rule2))] The bear is young.[(triple3)] @1: The bear is nice.[(((triple1 triple3) -> rule4) OR ((((triple3 triple2) -> rule6) triple3) -> rule4))] @2: The bear is rough.[(((triple3 ((triple1 triple3) -> rule4)) -> rule8) OR ((triple3 ((((triple3 triple2) -> rule6) triple3) -> rule4)) -> rule8))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
((triple3 triple2) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is red.
("bear" "is" "red" "+")
triple2
((((triple3 ((triple1 triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is young.
("bear" "is" "young" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple1 triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
((triple3 ((triple1 triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((triple3 ((((triple3 triple2) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3