The bear chases the cow. The cow needs the squirrel. The squirrel is red. If someone is red then they like the bear. If someone likes the bear then the bear is nice. If someone is red then they like the cow. If someone needs the cow and they are kind then the cow likes the squirrel. If someone is big then they are rough. If someone chases the squirrel and the squirrel needs the cow then the squirrel chases the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If someone is red then they like the bear.
((("someone" "is" "red" "+")) -> ("someone" "likes" "bear" "+"))
If someone likes the bear then the bear is nice.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "nice" "+"))
If someone is red then they like the cow.
((("someone" "is" "red" "+")) -> ("someone" "likes" "cow" "+"))
If someone needs the cow and they are kind then the cow likes the squirrel.
((("someone" "needs" "cow" "+") ("someone" "is" "kind" "+")) -> ("cow" "likes" "squirrel" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone chases the squirrel and the squirrel needs the cow then the squirrel chases the bear.
((("someone" "chases" "squirrel" "+") ("squirrel" "needs" "cow" "+")) -> ("squirrel" "chases" "bear" "+"))
The cow needs the squirrel.
True
1
proof
[(triple2)]
("cow" "needs" "squirrel" "+")
triple2
The squirrel is not red.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "red" "-")
triple3
The squirrel likes the cow.
True
2
proof
[(((triple3) -> rule3))]
("squirrel" "likes" "cow" "+")
((triple3) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel does not like the cow.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "likes" "cow" "-")
((triple3) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The bear is nice.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("bear" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear is not nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("bear" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "rough" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cow" "+")
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "bear" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cow does not chase the squirrel.
Unknown
inv-random
[@0: The cow chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "squirrel" "-")
The bear likes the squirrel.
Unknown
random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "+")
@0: The bear chases the cow.[(triple1)] The cow needs the squirrel.[(triple2)] The squirrel is red.[(triple3)] @1: The squirrel likes the bear.[(((triple3) -> rule1))] The squirrel likes the cow.[(((triple3) -> rule3))] @2: The bear is nice.[(((((triple3) -> rule1)) -> rule2))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
((triple3) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((triple3) -> (rule3 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2