The cow chases the rabbit. The cow chases the tiger. The cow does not need the mouse. The cow sees the rabbit. The mouse chases the tiger. The mouse needs the cow. The mouse needs the tiger. The mouse sees the rabbit. The rabbit chases the mouse. The rabbit does not chase the tiger. The rabbit is rough. The rabbit needs the tiger. The rabbit sees the cow. The rabbit sees the tiger. The tiger chases the rabbit. The tiger sees the rabbit. If something chases the cow then the cow does not need the rabbit. If something needs the rabbit and it sees the rabbit then the rabbit needs the mouse. If the rabbit does not see the cow and the rabbit does not need the cow then the cow needs the mouse. If something needs the tiger and it is not round then it chases the cow. If something is cold then it chases the tiger. If something chases the mouse then it sees the rabbit.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something chases the cow then the cow does not need the rabbit.
((("something" "chases" "cow" "+")) -> ("cow" "needs" "rabbit" "-"))
If something needs the rabbit and it sees the rabbit then the rabbit needs the mouse.
((("something" "needs" "rabbit" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If the rabbit does not see the cow and the rabbit does not need the cow then the cow needs the mouse.
((("rabbit" "sees" "cow" "~") ("rabbit" "needs" "cow" "~")) -> ("cow" "needs" "mouse" "+"))
If something needs the tiger and it is not round then it chases the cow.
((("something" "needs" "tiger" "+") ("something" "is" "round" "~")) -> ("something" "chases" "cow" "+"))
If something is cold then it chases the tiger.
((("something" "is" "cold" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the mouse then it sees the rabbit.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "rabbit" "+"))
The cow does not need the mouse.
True
1
proof
[(triple3)]
("cow" "needs" "mouse" "-")
triple3
The tiger does not see the rabbit.
False
1
inv-proof
[(triple16)]
("tiger" "sees" "rabbit" "-")
triple16
The rabbit sees the rabbit.
True
2
proof
[(((triple9) -> rule6))]
("rabbit" "sees" "rabbit" "+")
((triple9) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple9) -> rule6))]
("rabbit" "sees" "rabbit" "-")
((triple9) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The tiger does not chase the cow.
Unknown
inv-rconc
[@1: The tiger chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "cow" "-")
The mouse chases the cow.
Unknown
rconc
[@1: The mouse chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "cow" "+")
The cow does not need the rabbit.
Unknown
inv-random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow chases the rabbit.[(triple1)] The cow chases the tiger.[(triple2)] The cow does not need the mouse.[(triple3)] The cow sees the rabbit.[(triple4)] The mouse chases the tiger.[(triple5)] The mouse needs the cow.[(triple6)] The mouse needs the tiger.[(triple7)] The mouse sees the rabbit.[(triple8)] The rabbit chases the mouse.[(triple9)] The rabbit does not chase the tiger.[(triple10)] The rabbit is rough.[(triple11)] The rabbit needs the tiger.[(triple12)] The rabbit sees the cow.[(triple13)] The rabbit sees the tiger.[(triple14)] The tiger chases the rabbit.[(triple15)] The tiger sees the rabbit.[(triple16)] @1: The rabbit sees the rabbit.[(((triple9) -> rule6))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple2
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
triple3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple5
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple6
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple7
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple8
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple9
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple12
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple13
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple14
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple15
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple16
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple9) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1