The cat visits the rabbit. The rabbit is young. The rabbit visits the cat. If something likes the rabbit and the rabbit is nice then the rabbit is not green. If something is big then it visits the rabbit. If something likes the cat then it visits the rabbit. If the rabbit does not like the cat then the rabbit chases the cat. If something is big and it does not like the cat then the cat visits the rabbit. If something is green then it visits the cat. If something chases the cat and the cat does not like the rabbit then it is nice. If something is young and it visits the cat then the cat is big.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something likes the rabbit and the rabbit is nice then the rabbit is not green.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "nice" "+")) -> ("rabbit" "is" "green" "-"))
If something is big then it visits the rabbit.
((("something" "is" "big" "+")) -> ("something" "visits" "rabbit" "+"))
If something likes the cat then it visits the rabbit.
((("something" "likes" "cat" "+")) -> ("something" "visits" "rabbit" "+"))
If the rabbit does not like the cat then the rabbit chases the cat.
((("rabbit" "likes" "cat" "~")) -> ("rabbit" "chases" "cat" "+"))
If something is big and it does not like the cat then the cat visits the rabbit.
((("something" "is" "big" "+") ("something" "likes" "cat" "~")) -> ("cat" "visits" "rabbit" "+"))
If something is green then it visits the cat.
((("something" "is" "green" "+")) -> ("something" "visits" "cat" "+"))
If something chases the cat and the cat does not like the rabbit then it is nice.
((("something" "chases" "cat" "+") ("cat" "likes" "rabbit" "~")) -> ("something" "is" "nice" "+"))
If something is young and it visits the cat then the cat is big.
((("something" "is" "young" "+") ("something" "visits" "cat" "+")) -> ("cat" "is" "big" "+"))
The cat visits the rabbit.
True
1
proof
[(triple1 OR ((((triple2 triple3) -> rule8)) -> rule2))]
("cat" "visits" "rabbit" "+")
triple1
((((triple2 triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat does not visit the rabbit.
False
1
inv-proof
[(triple1 OR ((((triple2 triple3) -> rule8)) -> rule2))]
("cat" "visits" "rabbit" "-")
triple1
((((triple2 triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat is big.
True
3
proof
[(((triple2 triple3) -> rule8))]
("cat" "is" "big" "+")
((triple2 triple3) -> (rule8 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
3
inv-proof
[(((triple2 triple3) -> rule8))]
("cat" "is" "big" "-")
((triple2 triple3) -> (rule8 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "nice" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The rabbit likes the cat.
Unknown
random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "+")
@0: The cat visits the rabbit.[(triple1 OR ((((triple2 triple3) -> rule8)) -> rule2))] The rabbit is young.[(triple2)] The rabbit visits the cat.[(triple3)] @1: The cat is big.[(((triple2 triple3) -> rule8))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
((((triple2 triple3) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
triple2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple3
The cat is big.
("cat" "is" "big" "+")
((triple2 triple3) -> (rule8 % int1))
The cat is big.
("cat" "is" "big" "+")
int1