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