The cow is not round. The rabbit needs the cow. If something is green and it does not like the cow then it does not like the rabbit. If something is kind then it is red. If something chases the rabbit then the rabbit is green. If the cow needs the rabbit and the rabbit needs the cow then the rabbit is green. If something needs the cow then it chases the cow. If something is green then it chases the cow. If something chases the cow then the cow likes the rabbit. If something is kind and it likes the cow then the cow does not like the rabbit.
The cow is not round.
("cow" "is" "round" "-")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If something is green and it does not like the cow then it does not like the rabbit.
((("something" "is" "green" "+") ("something" "likes" "cow" "~")) -> ("something" "likes" "rabbit" "-"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something chases the rabbit then the rabbit is green.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If the cow needs the rabbit and the rabbit needs the cow then the rabbit is green.
((("cow" "needs" "rabbit" "+") ("rabbit" "needs" "cow" "+")) -> ("rabbit" "is" "green" "+"))
If something needs the cow then it chases the cow.
((("something" "needs" "cow" "+")) -> ("something" "chases" "cow" "+"))
If something is green then it chases the cow.
((("something" "is" "green" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cow then the cow likes the rabbit.
((("something" "chases" "cow" "+")) -> ("cow" "likes" "rabbit" "+"))
If something is kind and it likes the cow then the cow does not like the rabbit.
((("something" "is" "kind" "+") ("something" "likes" "cow" "+")) -> ("cow" "likes" "rabbit" "-"))
The rabbit needs the cow.
True
1
proof
[(triple2)]
("rabbit" "needs" "cow" "+")
triple2
The rabbit does not need the cow.
False
1
inv-proof
[(triple2)]
("rabbit" "needs" "cow" "-")
triple2
The rabbit chases the cow.
True
2
proof
[(((triple2) -> rule5))]
("rabbit" "chases" "cow" "+")
((triple2) -> (rule5 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule5))]
("rabbit" "chases" "cow" "-")
((triple2) -> (rule5 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow likes the rabbit.
True
3
proof
[(((((triple2) -> rule5)) -> rule7))]
("cow" "likes" "rabbit" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow does not like the rabbit.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule7))]
("cow" "likes" "rabbit" "-")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "red" "+")
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "green" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The rabbit does not like the cow.
Unknown
inv-random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cow is not round.[(triple1)] The rabbit needs the cow.[(triple2)] @1: The rabbit chases the cow.[(((triple2) -> rule5))] @2: The cow likes the rabbit.[(((((triple2) -> rule5)) -> rule7))]
The cow is not round.
("cow" "is" "round" "-")
triple1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple2) -> (rule5 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2