The cat eats the rabbit. The cow likes the cat. The cow does not need the cat. The mouse is kind. The mouse likes the rabbit. The rabbit does not eat the cat. The rabbit does not like the cat. If someone is round then they like the cat. If someone likes the cat then they eat the cat. If someone likes the cat then the cat is round. If someone needs the rabbit and the rabbit eats the cow then the rabbit is round. If the cow is not nice then the cow likes the mouse. If someone eats the rabbit and they do not like the rabbit then the rabbit is nice.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow does not need the cat.
("cow" "needs" "cat" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
If someone is round then they like the cat.
((("someone" "is" "round" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the cat then they eat the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If someone likes the cat then the cat is round.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone needs the rabbit and the rabbit eats the cow then the rabbit is round.
((("someone" "needs" "rabbit" "+") ("rabbit" "eats" "cow" "+")) -> ("rabbit" "is" "round" "+"))
If the cow is not nice then the cow likes the mouse.
((("cow" "is" "nice" "~")) -> ("cow" "likes" "mouse" "+"))
If someone eats the rabbit and they do not like the rabbit then the rabbit is nice.
((("someone" "eats" "rabbit" "+") ("someone" "likes" "rabbit" "~")) -> ("rabbit" "is" "nice" "+"))
The cow likes the cat.
True
1
proof
[(triple2)]
("cow" "likes" "cat" "+")
triple2
The cow needs the cat.
False
1
inv-proof
[(triple3)]
("cow" "needs" "cat" "+")
triple3
The cat is round.
True
2
proof
[(((triple2) -> rule3))]
("cat" "is" "round" "+")
((triple2) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cow does not eat the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "eats" "cat" "-")
((triple2) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cat likes the cat.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("cat" "likes" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not like the cat.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("cat" "likes" "cat" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat eats the cat.
True
4
proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule2))]
("cat" "eats" "cat" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat does not eat the cat.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule2))]
("cat" "eats" "cat" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "cat" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "round" "+")
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "nice" "-")
The cow likes the mouse.
Unknown
rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "mouse" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The cat likes the rabbit.
Unknown
random
[@0: The cat likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "rabbit" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The cat eats the rabbit.[(triple1)] The cow does not need the cat.[(triple3)] The cow likes the cat.[(triple2)] The mouse is kind.[(triple4)] The mouse likes the rabbit.[(triple5)] The rabbit does not eat the cat.[(triple6)] The rabbit does not like the cat.[(triple7)] @1: The cat is round.[(((triple2) -> rule3))] The cow eats the cat.[(((triple2) -> rule2))] @2: The cat likes the cat.[(((((triple2) -> rule3)) -> rule1))] @3: The cat eats the cat.[(((((((triple2) -> rule3)) -> rule1)) -> rule2))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cow does not need the cat.
("cow" "needs" "cat" "-")
triple3
The cow likes the cat.
("cow" "likes" "cat" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple5
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
triple6
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
triple7
The cat is round.
("cat" "is" "round" "+")
((triple2) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple2) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3