The dog is young. The rabbit likes the squirrel. The squirrel is young. If someone chases the dog then they chase the squirrel. If someone visits the squirrel then the squirrel chases the dog. If someone likes the dog and they chase the dog then the dog chases the squirrel. If someone likes the squirrel then the squirrel visits the rabbit. If someone is blue then they are red. If someone is rough then they like the rabbit. If someone visits the rabbit then the rabbit chases the dog. If someone likes the squirrel then the squirrel likes the rabbit.
The dog is young.
("dog" "is" "young" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If someone chases the dog then they chase the squirrel.
((("someone" "chases" "dog" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone visits the squirrel then the squirrel chases the dog.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "chases" "dog" "+"))
If someone likes the dog and they chase the dog then the dog chases the squirrel.
((("someone" "likes" "dog" "+") ("someone" "chases" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If someone likes the squirrel then the squirrel visits the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is rough then they like the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone visits the rabbit then the rabbit chases the dog.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If someone likes the squirrel then the squirrel likes the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
The rabbit likes the squirrel.
True
1
proof
[(triple2)]
("rabbit" "likes" "squirrel" "+")
triple2
The dog is not young.
False
1
inv-proof
[(triple1)]
("dog" "is" "young" "-")
triple1
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@2: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The rabbit visits the dog.
Unknown
random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "+")
@0: The dog is young.[(triple1)] The rabbit likes the squirrel.[(triple2)] The squirrel is young.[(triple3)] @1: The squirrel likes the rabbit.[(((triple2) -> rule8))] The squirrel visits the rabbit.[(((triple2) -> rule4))] @2: The rabbit chases the dog.[(((((triple2) -> rule4)) -> rule7))] @3: The rabbit chases the squirrel.[(((((((triple2) -> rule4)) -> rule7)) -> rule1))]
The dog is young.
("dog" "is" "young" "+")
triple1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple2) -> (rule8 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
((triple2) -> (rule4 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3