The cow chases the squirrel. The mouse does not visit the rabbit. The rabbit visits the mouse. The squirrel eats the cow. If someone eats the mouse then they are not rough. If someone chases the squirrel then the squirrel chases the mouse. If someone chases the rabbit and they do not eat the cow then they eat the mouse. If someone visits the cow then they are green. If someone eats the cow then the cow chases the mouse. If the rabbit does not eat the mouse then the mouse does not eat the squirrel. If the rabbit is not rough then the rabbit does not chase the mouse. If someone chases the mouse then they eat the squirrel.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
If someone eats the mouse then they are not rough.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "rough" "-"))
If someone chases the squirrel then the squirrel chases the mouse.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If someone chases the rabbit and they do not eat the cow then they eat the mouse.
((("someone" "chases" "rabbit" "+") ("someone" "eats" "cow" "~")) -> ("someone" "eats" "mouse" "+"))
If someone visits the cow then they are green.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "green" "+"))
If someone eats the cow then the cow chases the mouse.
((("someone" "eats" "cow" "+")) -> ("cow" "chases" "mouse" "+"))
If the rabbit does not eat the mouse then the mouse does not eat the squirrel.
((("rabbit" "eats" "mouse" "~")) -> ("mouse" "eats" "squirrel" "-"))
If the rabbit is not rough then the rabbit does not chase the mouse.
((("rabbit" "is" "rough" "~")) -> ("rabbit" "chases" "mouse" "-"))
If someone chases the mouse then they eat the squirrel.
((("someone" "chases" "mouse" "+")) -> ("someone" "eats" "squirrel" "+"))
The cow chases the squirrel.
True
1
proof
[(triple1)]
("cow" "chases" "squirrel" "+")
triple1
The mouse visits the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "rabbit" "+")
triple2
The cow chases the mouse.
True
2
proof
[(((triple4) -> rule5))]
("cow" "chases" "mouse" "+")
((triple4) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The squirrel does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("squirrel" "chases" "mouse" "-")
((triple1) -> (rule2 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel eats the squirrel.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("squirrel" "eats" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The cow does not eat the squirrel.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule8))]
("cow" "eats" "squirrel" "-")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The mouse does not eat the squirrel.
Unknown
inv-rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "squirrel" "-")
The cow eats the mouse.
Unknown
rconc
[@1: The cow eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "mouse" "+")
The rabbit does not eat the mouse.
Unknown
inv-rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "mouse" "-")
The mouse chases the cow.
Unknown
random
[@0: The mouse chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cow" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The mouse visits the squirrel.
Unknown
random
[@0: The mouse visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "squirrel" "+")
@0: The cow chases the squirrel.[(triple1)] The mouse does not visit the rabbit.[(triple2)] The rabbit visits the mouse.[(triple3)] The squirrel eats the cow.[(triple4)] @1: The cow chases the mouse.[(((triple4) -> rule5))] The squirrel chases the mouse.[(((triple1) -> rule2))] @2: The cow eats the squirrel.[(((((triple4) -> rule5)) -> rule8))] The squirrel eats the squirrel.[(((((triple1) -> rule2)) -> rule8))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple4
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((triple4) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((triple1) -> (rule2 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2