The bear is kind. The bear is nice. The bear is red. The bear is round. The bear is young. All red, young things are nice. Young, kind things are red. All kind things are nice. All young, red things are kind. If something is young then it is round. If the bear is red then the bear is nice.
The bear is kind.
("bear" "is" "kind" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
All red, young things are nice.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Young, kind things are red.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All young, red things are kind.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If the bear is red then the bear is nice.
((("bear" "is" "red" "+")) -> ("bear" "is" "nice" "+"))
The bear is nice.
True
1
proof
[(triple2 OR ((triple1) -> rule3) OR ((triple3) -> rule6) OR ((triple3 triple5) -> rule1) OR ((((triple5 triple1) -> rule2)) -> rule6) OR ((((triple5 triple3) -> rule4)) -> rule3) OR ((((triple5 triple1) -> rule2) triple5) -> rule1))]
("bear" "is" "nice" "+")
triple2
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple3) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple3 triple5) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
((((triple5 triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple5 triple1) -> (rule2 % int2)) triple5) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is not nice.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule3) OR ((triple3) -> rule6) OR ((triple3 triple5) -> rule1) OR ((((triple5 triple1) -> rule2)) -> rule6) OR ((((triple5 triple3) -> rule4)) -> rule3) OR ((((triple5 triple1) -> rule2) triple5) -> rule1))]
("bear" "is" "nice" "-")
triple2
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple3) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple3 triple5) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
((((triple5 triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple5 triple1) -> (rule2 % int2)) triple5) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is kind.[(triple1 OR ((triple5 triple3) -> rule4))] The bear is nice.[(triple2 OR ((triple1) -> rule3) OR ((triple3) -> rule6) OR ((triple3 triple5) -> rule1) OR ((((triple5 triple1) -> rule2)) -> rule6) OR ((((triple5 triple3) -> rule4)) -> rule3) OR ((((triple5 triple1) -> rule2) triple5) -> rule1))] The bear is red.[(triple3 OR ((triple5 triple1) -> rule2))] The bear is round.[(triple4 OR ((triple5) -> rule5))] The bear is young.[(triple5)]
The bear is kind.
("bear" "is" "kind" "+")
triple1
((triple5 triple3) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
triple2
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple3) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple3 triple5) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
((((triple5 triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple5 triple1) -> (rule2 % int2)) triple5) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is red.
("bear" "is" "red" "+")
triple3
((triple5 triple1) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple4
((triple5) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is young.
("bear" "is" "young" "+")
triple5