The cat chases the rabbit. The cat is blue. The cat is nice. The cat is round. The cat likes the rabbit. The cat needs the rabbit. The rabbit chases the cat. The rabbit is not blue. The rabbit is round. The rabbit does not need the cat. If something likes the rabbit then it chases the cat. If something likes the cat and it needs the rabbit then the cat needs the rabbit. If something needs the rabbit then the rabbit chases the cat. If something likes the cat then it is round. If something needs the rabbit and it is not round then the rabbit does not need the cat. If the rabbit is rough then the rabbit needs the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
If something likes the rabbit then it chases the cat.
((("something" "likes" "rabbit" "+")) -> ("something" "chases" "cat" "+"))
If something likes the cat and it needs the rabbit then the cat needs the rabbit.
((("something" "likes" "cat" "+") ("something" "needs" "rabbit" "+")) -> ("cat" "needs" "rabbit" "+"))
If something needs the rabbit then the rabbit chases the cat.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "chases" "cat" "+"))
If something likes the cat then it is round.
((("something" "likes" "cat" "+")) -> ("something" "is" "round" "+"))
If something needs the rabbit and it is not round then the rabbit does not need the cat.
((("something" "needs" "rabbit" "+") ("something" "is" "round" "~")) -> ("rabbit" "needs" "cat" "-"))
If the rabbit is rough then the rabbit needs the cat.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "needs" "cat" "+"))
The rabbit chases the cat.
True
1
proof
[(triple7 OR ((triple6) -> rule3))]
("rabbit" "chases" "cat" "+")
triple7
((triple6) -> (rule3 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The cat is not nice.
False
1
inv-proof
[(triple3)]
("cat" "is" "nice" "-")
triple3
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is blue.[(triple2)] The cat is nice.[(triple3)] The cat is round.[(triple4)] The cat likes the rabbit.[(triple5)] The cat needs the rabbit.[(triple6)] The rabbit chases the cat.[(triple7 OR ((triple6) -> rule3))] The rabbit does not need the cat.[(triple10)] The rabbit is not blue.[(triple8)] The rabbit is round.[(triple9)] @1: The cat chases the cat.[(((triple5) -> rule1))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple7
((triple6) -> (rule3 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
triple10
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple5) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1