The cat does not chase the squirrel. The squirrel likes the tiger. The tiger likes the cat. If the cat chases the tiger then the tiger sees the squirrel. If someone likes the tiger then the tiger sees the squirrel. If someone is rough then they like the tiger. If someone chases the tiger and the tiger sees the cat then the tiger likes the squirrel. If someone is cold and they like the cat then they are round. If the cat is not rough and the cat does not chase the squirrel then the squirrel chases the tiger.
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If the cat chases the tiger then the tiger sees the squirrel.
((("cat" "chases" "tiger" "+")) -> ("tiger" "sees" "squirrel" "+"))
If someone likes the tiger then the tiger sees the squirrel.
((("someone" "likes" "tiger" "+")) -> ("tiger" "sees" "squirrel" "+"))
If someone is rough then they like the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "tiger" "+"))
If someone chases the tiger and the tiger sees the cat then the tiger likes the squirrel.
((("someone" "chases" "tiger" "+") ("tiger" "sees" "cat" "+")) -> ("tiger" "likes" "squirrel" "+"))
If someone is cold and they like the cat then they are round.
((("someone" "is" "cold" "+") ("someone" "likes" "cat" "+")) -> ("someone" "is" "round" "+"))
If the cat is not rough and the cat does not chase the squirrel then the squirrel chases the tiger.
((("cat" "is" "rough" "~") ("cat" "chases" "squirrel" "~")) -> ("squirrel" "chases" "tiger" "+"))
The cat does not chase the squirrel.
True
1
proof
[(triple1)]
("cat" "chases" "squirrel" "-")
triple1
The tiger does not like the cat.
False
1
inv-proof
[(triple3)]
("tiger" "likes" "cat" "-")
triple3
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat does not chase the squirrel.[(triple1)] The squirrel likes the tiger.[(triple2)] The tiger likes the cat.[(triple3)] @1: The tiger sees the squirrel.[(((triple2) -> rule2))]
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
triple1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple3
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((triple2) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1