The cat does not chase the cow. The cat chases the rabbit. The cat likes the cow. The cat needs the rabbit. The cow is blue. The cow needs the cat. The rabbit needs the cat. If the cow needs the cat and the cat needs the rabbit then the cat needs the cow. If something is rough and it chases the rabbit then the rabbit likes the cow. If something is rough and it does not need the cat then it needs the cow. If something is big and it does not need the rabbit then it chases the cow. If something likes the rabbit and it is rough then it is not round. If something is red then it chases the rabbit. If something needs the cat then it likes the cow. If the rabbit is rough then the rabbit is blue.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If the cow needs the cat and the cat needs the rabbit then the cat needs the cow.
((("cow" "needs" "cat" "+") ("cat" "needs" "rabbit" "+")) -> ("cat" "needs" "cow" "+"))
If something is rough and it chases the rabbit then the rabbit likes the cow.
((("something" "is" "rough" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "likes" "cow" "+"))
If something is rough and it does not need the cat then it needs the cow.
((("something" "is" "rough" "+") ("something" "needs" "cat" "~")) -> ("something" "needs" "cow" "+"))
If something is big and it does not need the rabbit then it chases the cow.
((("something" "is" "big" "+") ("something" "needs" "rabbit" "~")) -> ("something" "chases" "cow" "+"))
If something likes the rabbit and it is rough then it is not round.
((("something" "likes" "rabbit" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
If something is red then it chases the rabbit.
((("something" "is" "red" "+")) -> ("something" "chases" "rabbit" "+"))
If something needs the cat then it likes the cow.
((("something" "needs" "cat" "+")) -> ("something" "likes" "cow" "+"))
If the rabbit is rough then the rabbit is blue.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "blue" "+"))
The rabbit needs the cat.
True
1
proof
[(triple7)]
("rabbit" "needs" "cat" "+")
triple7
The cat does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("cat" "chases" "rabbit" "-")
triple2
The cow likes the cow.
True
2
proof
[(((triple6) -> rule7))]
("cow" "likes" "cow" "+")
((triple6) -> (rule7 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The rabbit does not like the cow.
False
2
inv-proof
[(((triple7) -> rule7))]
("rabbit" "likes" "cow" "-")
((triple7) -> (rule7 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cow" "-")
The rabbit needs the cow.
Unknown
rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "cow" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The rabbit chases the cat.
Unknown
random
[@0: The rabbit chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cat" "+")
@0: The cat chases the rabbit.[(triple2)] The cat does not chase the cow.[(triple1)] The cat likes the cow.[(triple3)] The cat needs the rabbit.[(triple4)] The cow is blue.[(triple5)] The cow needs the cat.[(triple6)] The rabbit needs the cat.[(triple7)] @1: The cat needs the cow.[(((triple6 triple4) -> rule1))] The cow likes the cow.[(((triple6) -> rule7))] The rabbit likes the cow.[(((triple7) -> rule7))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow needs the cat.
("cow" "needs" "cat" "+")
triple6
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple7
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple6 triple4) -> (rule1 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple6) -> (rule7 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
((triple7) -> (rule7 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1