The cat is red. The cat likes the cow. The cat does not like the tiger. The cow chases the tiger. The squirrel is red. The tiger is kind. The tiger likes the squirrel. If someone eats the tiger and they eat the cat then they do not eat the squirrel. If someone eats the squirrel then they are not red. If someone eats the cow then the cow chases the tiger. If someone chases the cow then they do not like the cow. If someone is kind then they chase the cat. If the cat chases the tiger then the cat does not chase the cow.
The cat is red.
("cat" "is" "red" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If someone eats the tiger and they eat the cat then they do not eat the squirrel.
((("someone" "eats" "tiger" "+") ("someone" "eats" "cat" "+")) -> ("someone" "eats" "squirrel" "-"))
If someone eats the squirrel then they are not red.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "red" "-"))
If someone eats the cow then the cow chases the tiger.
((("someone" "eats" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If someone chases the cow then they do not like the cow.
((("someone" "chases" "cow" "+")) -> ("someone" "likes" "cow" "-"))
If someone is kind then they chase the cat.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "cat" "+"))
If the cat chases the tiger then the cat does not chase the cow.
((("cat" "chases" "tiger" "+")) -> ("cat" "chases" "cow" "-"))
The cow chases the tiger.
True
1
proof
[(triple4)]
("cow" "chases" "tiger" "+")
triple4
The squirrel is not red.
False
1
inv-proof
[(triple5)]
("squirrel" "is" "red" "-")
triple5
The tiger chases the cat.
True
2
proof
[(((triple6) -> rule5))]
("tiger" "chases" "cat" "+")
((triple6) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger does not chase the cat.
False
2
inv-proof
[(((triple6) -> rule5))]
("tiger" "chases" "cat" "-")
((triple6) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "cat" "-")
The squirrel chases the cat.
Unknown
rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "cat" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cow chases the squirrel.
Unknown
random
[@0: The cow chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "squirrel" "+")
@0: The cat does not like the tiger.[(triple3)] The cat is red.[(triple1)] The cat likes the cow.[(triple2)] The cow chases the tiger.[(triple4)] The squirrel is red.[(triple5)] The tiger is kind.[(triple6)] The tiger likes the squirrel.[(triple7)] @1: The tiger chases the cat.[(((triple6) -> rule5))]
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
triple3
The cat is red.
("cat" "is" "red" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple4
The squirrel is red.
("squirrel" "is" "red" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple7
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple6) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1