The cow is round. The cow needs the rabbit. The mouse eats the cow. The mouse is blue. The mouse is not red. The mouse is not rough. The mouse needs the rabbit. The mouse visits the rabbit. The rabbit does not eat the cow. The rabbit eats the mouse. The rabbit visits the cow. The rabbit visits the mouse. If someone needs the cow and they are not red then they do not eat the rabbit. If someone needs the cow then they visit the rabbit. If someone visits the cow and they need the cow then the cow needs the mouse. If someone visits the rabbit then they need the rabbit. If the mouse eats the rabbit then the mouse is blue. If someone visits the mouse and the mouse is not rough then the mouse visits the cow.
The cow is round.
("cow" "is" "round" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone needs the cow and they are not red then they do not eat the rabbit.
((("someone" "needs" "cow" "+") ("someone" "is" "red" "~")) -> ("someone" "eats" "rabbit" "-"))
If someone needs the cow then they visit the rabbit.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the cow and they need the cow then the cow needs the mouse.
((("someone" "visits" "cow" "+") ("someone" "needs" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
If someone visits the rabbit then they need the rabbit.
((("someone" "visits" "rabbit" "+")) -> ("someone" "needs" "rabbit" "+"))
If the mouse eats the rabbit then the mouse is blue.
((("mouse" "eats" "rabbit" "+")) -> ("mouse" "is" "blue" "+"))
If someone visits the mouse and the mouse is not rough then the mouse visits the cow.
((("someone" "visits" "mouse" "+") ("mouse" "is" "rough" "~")) -> ("mouse" "visits" "cow" "+"))
The cow is round.
True
1
proof
[(triple1)]
("cow" "is" "round" "+")
triple1
The mouse does not need the rabbit.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule4))]
("mouse" "needs" "rabbit" "-")
triple7
((triple8) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse visits the cow.
True
3
proof
[(((triple12 triple6) -> rule6))]
("mouse" "visits" "cow" "+")
((triple12 triple6) -> (rule6 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse does not visit the cow.
False
3
inv-proof
[(((triple12 triple6) -> rule6))]
("mouse" "visits" "cow" "-")
((triple12 triple6) -> (rule6 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow does not need the mouse.
Unknown
inv-rconc
[@1: The cow needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "mouse" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cow is round.[(triple1)] The cow needs the rabbit.[(triple2)] The mouse eats the cow.[(triple3)] The mouse is blue.[(triple4)] The mouse is not red.[(triple5)] The mouse is not rough.[(triple6)] The mouse needs the rabbit.[(triple7 OR ((triple8) -> rule4))] The mouse visits the rabbit.[(triple8)] The rabbit does not eat the cow.[(triple9)] The rabbit eats the mouse.[(triple10)] The rabbit visits the cow.[(triple11)] The rabbit visits the mouse.[(triple12)] @1: The mouse visits the cow.[(((triple12 triple6) -> rule6))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is not red.
("mouse" "is" "red" "-")
triple5
The mouse is not rough.
("mouse" "is" "rough" "-")
triple6
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple7
((triple8) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
triple9
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple10
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple11
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((triple12 triple6) -> (rule6 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1