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