The bald eagle needs the rabbit. The cat chases the rabbit. The cow needs the cat. The rabbit chases the cat. If someone chases the cow and the cow chases the cat then the cow is green. If someone chases the rabbit then they are rough. If someone needs the cat and they need the cow then the cat is round.
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
If someone chases the cow and the cow chases the cat then the cow is green.
((("someone" "chases" "cow" "+") ("cow" "chases" "cat" "+")) -> ("cow" "is" "green" "+"))
If someone chases the rabbit then they are rough.
((("someone" "chases" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the cat and they need the cow then the cat is round.
((("someone" "needs" "cat" "+") ("someone" "needs" "cow" "+")) -> ("cat" "is" "round" "+"))
The cow needs the cat.
True
1
proof
[(triple3)]
("cow" "needs" "cat" "+")
triple3
The cat does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("cat" "chases" "rabbit" "-")
triple2
The cat is rough.
True
2
proof
[(((triple2) -> rule2))]
("cat" "is" "rough" "+")
((triple2) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "is" "rough" "-")
((triple2) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "rough" "-")
The cow is green.
Unknown
rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "green" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
@0: The bald eagle needs the rabbit.[(triple1)] The cat chases the rabbit.[(triple2)] The cow needs the cat.[(triple3)] The rabbit chases the cat.[(triple4)] @1: The cat is rough.[(((triple2) -> rule2))]
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cow needs the cat.
("cow" "needs" "cat" "+")
triple3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
((triple2) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1