The cat likes the squirrel. The dog sees the tiger. The squirrel is kind. The tiger visits the cat. If the cat sees the squirrel and the cat is kind then the squirrel does not visit the cat. If someone likes the cat then the cat sees the squirrel. If someone is kind then they visit the tiger. If someone likes the squirrel and the squirrel does not like the tiger then they visit the tiger. If someone is kind then they like the cat. If the squirrel does not see the dog then the dog likes the tiger. If someone visits the cat and they see the cat then the cat sees the tiger. If someone is green then they visit the squirrel.
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the cat sees the squirrel and the cat is kind then the squirrel does not visit the cat.
((("cat" "sees" "squirrel" "+") ("cat" "is" "kind" "+")) -> ("squirrel" "visits" "cat" "-"))
If someone likes the cat then the cat sees the squirrel.
((("someone" "likes" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If someone is kind then they visit the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "tiger" "+"))
If someone likes the squirrel and the squirrel does not like the tiger then they visit the tiger.
((("someone" "likes" "squirrel" "+") ("squirrel" "likes" "tiger" "~")) -> ("someone" "visits" "tiger" "+"))
If someone is kind then they like the cat.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "cat" "+"))
If the squirrel does not see the dog then the dog likes the tiger.
((("squirrel" "sees" "dog" "~")) -> ("dog" "likes" "tiger" "+"))
If someone visits the cat and they see the cat then the cat sees the tiger.
((("someone" "visits" "cat" "+") ("someone" "sees" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If someone is green then they visit the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "visits" "squirrel" "+"))
The tiger visits the cat.
True
1
proof
[(triple4)]
("tiger" "visits" "cat" "+")
triple4
The cat does not like the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "likes" "squirrel" "-")
triple1
The squirrel likes the cat.
True
2
proof
[(((triple3) -> rule5))]
("squirrel" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "visits" "tiger" "-")
((triple3) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The cat sees the squirrel.
True
3
proof
[(((((triple3) -> rule5)) -> rule2))]
("cat" "sees" "squirrel" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The cat does not see the squirrel.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule2))]
("cat" "sees" "squirrel" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The dog does not like the cat.
Unknown
inv-rconc
[@1: The dog likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "cat" "-")
The dog visits the tiger.
Unknown
rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "tiger" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel likes the dog.
Unknown
random
[@0: The squirrel likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "dog" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The cat likes the squirrel.[(triple1)] The dog sees the tiger.[(triple2)] The squirrel is kind.[(triple3)] The tiger visits the cat.[(triple4)] @1: The squirrel likes the cat.[(((triple3) -> rule5))] The squirrel visits the tiger.[(((triple3) -> rule3))] @2: The cat sees the squirrel.[(((((triple3) -> rule5)) -> rule2))]
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple4
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2