The cat does not chase the squirrel. The rabbit chases the cat. The squirrel does not visit the rabbit. If something chases the cat then it eats the rabbit. If something eats the rabbit then it eats the cat. If something chases the cat and it eats the rabbit then it eats the cat. Nice things are not kind. If the squirrel is nice and the squirrel visits the cat then the cat chases the rabbit. If the cat is nice then the cat visits the squirrel. If something is green and it visits the rabbit then the rabbit visits the cat. If something is nice and it eats the rabbit then it visits the cat.
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
If something chases the cat then it eats the rabbit.
((("something" "chases" "cat" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the rabbit then it eats the cat.
((("something" "eats" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
If something chases the cat and it eats the rabbit then it eats the cat.
((("something" "chases" "cat" "+") ("something" "eats" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
Nice things are not kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "-"))
If the squirrel is nice and the squirrel visits the cat then the cat chases the rabbit.
((("squirrel" "is" "nice" "+") ("squirrel" "visits" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If the cat is nice then the cat visits the squirrel.
((("cat" "is" "nice" "+")) -> ("cat" "visits" "squirrel" "+"))
If something is green and it visits the rabbit then the rabbit visits the cat.
((("something" "is" "green" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "cat" "+"))
If something is nice and it eats the rabbit then it visits the cat.
((("something" "is" "nice" "+") ("something" "eats" "rabbit" "+")) -> ("something" "visits" "cat" "+"))
The squirrel does not visit the rabbit.
True
1
proof
[(triple3)]
("squirrel" "visits" "rabbit" "-")
triple3
The cat chases the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "chases" "squirrel" "+")
triple1
The rabbit eats the rabbit.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "eats" "rabbit" "+")
((triple2) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "eats" "rabbit" "-")
((triple2) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the cat.
True
3
proof
[(((((triple2) -> rule1)) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule3))]
("rabbit" "eats" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit does not eat the cat.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule3))]
("rabbit" "eats" "cat" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The cat does not eat the cat.
Unknown
inv-rconc
[@2: The cat eats the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The cat eats the rabbit.
Unknown
rconc
[@1: The cat eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "rabbit" "+")
The squirrel does not eat the rabbit.
Unknown
inv-rconc
[@1: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "rabbit" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cat does not chase the squirrel.[(triple1)] The rabbit chases the cat.[(triple2)] The squirrel does not visit the rabbit.[(triple3)] @1: The rabbit eats the rabbit.[(((triple2) -> rule1))] @2: The rabbit eats the cat.[(((((triple2) -> rule1)) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule3))]
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
triple1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple2
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
triple3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple2) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2