The cow needs the mouse. The mouse chases the rabbit. The rabbit is young. If someone needs the mouse then they chase the mouse. If someone chases the mouse then the mouse is not blue.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If someone needs the mouse then they chase the mouse.
((("someone" "needs" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the mouse then the mouse is not blue.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "blue" "-"))
The cow needs the mouse.
True
1
proof
[(triple1)]
("cow" "needs" "mouse" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "young" "-")
triple3
The cow chases the mouse.
True
2
proof
[(((triple1) -> rule1))]
("cow" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "chases" "mouse" "-")
((triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The mouse is not blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("mouse" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The mouse is blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("mouse" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The cow does not like the mouse.
Unknown
inv-random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not chase the rabbit.
Unknown
inv-random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
@0: The cow needs the mouse.[(triple1)] The mouse chases the rabbit.[(triple2)] The rabbit is young.[(triple3)] @1: The cow chases the mouse.[(((triple1) -> rule1))] @2: The mouse is not blue.[(((((triple1) -> rule1)) -> rule2))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple2
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The mouse is not blue.
("mouse" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2