The cat visits the rabbit. The dog sees the rabbit. The rabbit does not see the squirrel. The squirrel sees the dog. If something is big then it does not eat the rabbit. If something visits the rabbit then it is rough. If something is kind then it is round. If the squirrel does not eat the cat then the cat is rough. If something visits the rabbit and it is young then the rabbit eats the cat. If something is rough then it eats the squirrel. If something eats the rabbit then it sees the squirrel. If the squirrel eats the cat and the squirrel does not visit the cat then the cat does not see the squirrel.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If something is big then it does not eat the rabbit.
((("something" "is" "big" "+")) -> ("something" "eats" "rabbit" "-"))
If something visits the rabbit then it is rough.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If the squirrel does not eat the cat then the cat is rough.
((("squirrel" "eats" "cat" "~")) -> ("cat" "is" "rough" "+"))
If something visits the rabbit and it is young then the rabbit eats the cat.
((("something" "visits" "rabbit" "+") ("something" "is" "young" "+")) -> ("rabbit" "eats" "cat" "+"))
If something is rough then it eats the squirrel.
((("something" "is" "rough" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the rabbit then it sees the squirrel.
((("something" "eats" "rabbit" "+")) -> ("something" "sees" "squirrel" "+"))
If the squirrel eats the cat and the squirrel does not visit the cat then the cat does not see the squirrel.
((("squirrel" "eats" "cat" "+") ("squirrel" "visits" "cat" "~")) -> ("cat" "sees" "squirrel" "-"))
The dog sees the rabbit.
True
1
proof
[(triple2)]
("dog" "sees" "rabbit" "+")
triple2
The rabbit sees the squirrel.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "squirrel" "+")
triple3
The cat is rough.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "rough" "-")
((triple1) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat eats the squirrel.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "eats" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat does not eat the squirrel.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "eats" "squirrel" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit eats the cat.
Unknown
rconc
[@1: The rabbit eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "cat" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cat visits the rabbit.[(triple1)] The dog sees the rabbit.[(triple2)] The rabbit does not see the squirrel.[(triple3)] The squirrel sees the dog.[(triple4)] @1: The cat is rough.[(((triple1) -> rule2))] @2: The cat eats the squirrel.[(((((triple1) -> rule2)) -> rule6))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple2
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
triple3
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2