The cow chases the rabbit. The cow is not red. The cow is young. The mouse is young. The mouse does not need the cow. The rabbit chases the mouse. The rabbit is young. If something is young and it eats the cow then the cow does not chase the mouse. If something chases the mouse then the mouse eats the rabbit. If something needs the cow then the cow needs the rabbit. If something is red then it chases the mouse. If the mouse eats the rabbit and the mouse needs the cow then the cow is blue. If the rabbit chases the cow then the cow chases the rabbit. If something is round and it does not eat the rabbit then it does not chase the rabbit. If something is young and not big then it does not chase the rabbit.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is not red.
("cow" "is" "red" "-")
The cow is young.
("cow" "is" "young" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If something is young and it eats the cow then the cow does not chase the mouse.
((("something" "is" "young" "+") ("something" "eats" "cow" "+")) -> ("cow" "chases" "mouse" "-"))
If something chases the mouse then the mouse eats the rabbit.
((("something" "chases" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
If something needs the cow then the cow needs the rabbit.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "rabbit" "+"))
If something is red then it chases the mouse.
((("something" "is" "red" "+")) -> ("something" "chases" "mouse" "+"))
If the mouse eats the rabbit and the mouse needs the cow then the cow is blue.
((("mouse" "eats" "rabbit" "+") ("mouse" "needs" "cow" "+")) -> ("cow" "is" "blue" "+"))
If the rabbit chases the cow then the cow chases the rabbit.
((("rabbit" "chases" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If something is round and it does not eat the rabbit then it does not chase the rabbit.
((("something" "is" "round" "+") ("something" "eats" "rabbit" "~")) -> ("something" "chases" "rabbit" "-"))
If something is young and not big then it does not chase the rabbit.
((("something" "is" "young" "+") ("something" "is" "big" "~")) -> ("something" "chases" "rabbit" "-"))
The cow chases the rabbit.
True
1
proof
[(triple1)]
("cow" "chases" "rabbit" "+")
triple1
The cow is not young.
False
1
inv-proof
[(triple3)]
("cow" "is" "young" "-")
triple3
The cow does not chase the mouse.
Unknown
inv-rconc
[@1: The cow chases the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "mouse" "-")
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 chases the rabbit.[(triple1)] The cow is not red.[(triple2)] The cow is young.[(triple3)] The mouse does not need the cow.[(triple5)] The mouse is young.[(triple4)] The rabbit chases the mouse.[(triple6)] The rabbit is young.[(triple7)] @1: The mouse eats the rabbit.[(((triple6) -> rule2))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is not red.
("cow" "is" "red" "-")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple4
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
((triple6) -> (rule2 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1