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