The cat visits the rabbit. The rabbit is big. If someone eats the cat then the cat does not need the rabbit. If someone visits the rabbit then the rabbit eats the cat. If someone visits the rabbit and they eat the cat then the rabbit is not kind.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If someone eats the cat then the cat does not need the rabbit.
((("someone" "eats" "cat" "+")) -> ("cat" "needs" "rabbit" "-"))
If someone visits the rabbit then the rabbit eats the cat.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "eats" "cat" "+"))
If someone visits the rabbit and they eat the cat then the rabbit is not kind.
((("someone" "visits" "rabbit" "+") ("someone" "eats" "cat" "+")) -> ("rabbit" "is" "kind" "-"))
The cat visits the rabbit.
True
1
proof
[(triple1)]
("cat" "visits" "rabbit" "+")
triple1
The rabbit is not big.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "big" "-")
triple2
The rabbit eats the cat.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "eats" "cat" "+")
((triple1) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit does not eat the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "eats" "cat" "-")
((triple1) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat does not need the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("cat" "needs" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The cat needs the rabbit.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("cat" "needs" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat visits the rabbit.[(triple1)] The rabbit is big.[(triple2)] @1: The rabbit eats the cat.[(((triple1) -> rule2))] @2: The cat does not need the rabbit.[(((((triple1) -> rule2)) -> rule1))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((triple1) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2