The cat eats the rabbit. The cat does not like the rabbit. The rabbit is kind. If someone likes the rabbit and they are rough then the rabbit sees the cat. If someone eats the rabbit and they are rough then they do not see the cat. If someone is big and not kind then they see the cat. If someone is big then they see the cat. If the rabbit likes the cat then the rabbit is round. If someone is kind then they like the rabbit. If someone is nice then they like the rabbit. If someone likes the rabbit then they are big.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If someone likes the rabbit and they are rough then the rabbit sees the cat.
((("someone" "likes" "rabbit" "+") ("someone" "is" "rough" "+")) -> ("rabbit" "sees" "cat" "+"))
If someone eats the rabbit and they are rough then they do not see the cat.
((("someone" "eats" "rabbit" "+") ("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "-"))
If someone is big and not kind then they see the cat.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "sees" "cat" "+"))
If someone is big then they see the cat.
((("someone" "is" "big" "+")) -> ("someone" "sees" "cat" "+"))
If the rabbit likes the cat then the rabbit is round.
((("rabbit" "likes" "cat" "+")) -> ("rabbit" "is" "round" "+"))
If someone is kind then they like the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone is nice then they like the rabbit.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the rabbit then they are big.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "big" "+"))
The rabbit is kind.
True
1
proof
[(triple3)]
("rabbit" "is" "kind" "+")
triple3
The cat does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "eats" "rabbit" "-")
triple1
The rabbit likes the rabbit.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "likes" "rabbit" "-")
((triple3) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
True
3
proof
[(((((triple3) -> rule6)) -> rule8))]
("rabbit" "is" "big" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule8))]
("rabbit" "is" "big" "-")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "big" "-")
The cat sees the cat.
Unknown
rconc
[@2: The cat sees the cat.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cat" "sees" "cat" "+")
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "round" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The rabbit eats the cat.
Unknown
random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "+")
@0: The cat does not like the rabbit.[(triple2)] The cat eats the rabbit.[(triple1)] The rabbit is kind.[(triple3)] @1: The rabbit likes the rabbit.[(((triple3) -> rule6))] @2: The rabbit is big.[(((((triple3) -> rule6)) -> rule8))] @3: The rabbit sees the cat.[(((((((triple3) -> rule6)) -> rule8)) -> rule4))]
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
triple2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3