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