The cow needs the mouse. The mouse chases the cow. The tiger visits the mouse. If the mouse visits the cow and the cow is cold then the cow visits the mouse. If someone is round then they are cold. If someone chases the tiger and they visit the cow then the cow chases the tiger. If the cow is young and the cow is cold then the cow visits the tiger. If someone needs the mouse then the mouse visits the cow. If someone chases the mouse and the mouse visits the tiger then the tiger is cold.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If the mouse visits the cow and the cow is cold then the cow visits the mouse.
((("mouse" "visits" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "visits" "mouse" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the tiger and they visit the cow then the cow chases the tiger.
((("someone" "chases" "tiger" "+") ("someone" "visits" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If the cow is young and the cow is cold then the cow visits the tiger.
((("cow" "is" "young" "+") ("cow" "is" "cold" "+")) -> ("cow" "visits" "tiger" "+"))
If someone needs the mouse then the mouse visits the cow.
((("someone" "needs" "mouse" "+")) -> ("mouse" "visits" "cow" "+"))
If someone chases the mouse and the mouse visits the tiger then the tiger is cold.
((("someone" "chases" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
The cow needs the mouse.
True
1
proof
[(triple1)]
("cow" "needs" "mouse" "+")
triple1
The mouse does not chase the cow.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "cow" "-")
triple2
The mouse visits the cow.
True
2
proof
[(((triple1) -> rule5))]
("mouse" "visits" "cow" "+")
((triple1) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse does not visit the cow.
False
2
inv-proof
[(((triple1) -> rule5))]
("mouse" "visits" "cow" "-")
((triple1) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "cold" "+")
The tiger does not chase the cow.
Unknown
inv-random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "-")
The mouse needs the cow.
Unknown
random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "+")
@0: The cow needs the mouse.[(triple1)] The mouse chases the cow.[(triple2)] The tiger visits the mouse.[(triple3)] @1: The mouse visits the cow.[(((triple1) -> rule5))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((triple1) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1