The cow does not chase the mouse. The cow needs the tiger. The cow sees the mouse. The mouse chases the cow. The mouse chases the tiger. The mouse needs the cow. The tiger is green. If someone needs the tiger then they need the cow. If someone is young and they do not see the cow then they are big. If someone sees the cow then the cow chases the mouse.
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone needs the tiger then they need the cow.
((("someone" "needs" "tiger" "+")) -> ("someone" "needs" "cow" "+"))
If someone is young and they do not see the cow then they are big.
((("someone" "is" "young" "+") ("someone" "sees" "cow" "~")) -> ("someone" "is" "big" "+"))
If someone sees the cow then the cow chases the mouse.
((("someone" "sees" "cow" "+")) -> ("cow" "chases" "mouse" "+"))
The mouse needs the cow.
True
1
proof
[(triple6)]
("mouse" "needs" "cow" "+")
triple6
The cow does not need the tiger.
False
1
inv-proof
[(triple2)]
("cow" "needs" "tiger" "-")
triple2
The cow needs the cow.
True
2
proof
[(((triple2) -> rule1))]
("cow" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "needs" "cow" "-")
((triple2) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "-")
The tiger needs the cow.
Unknown
rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "cow" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cow does not chase the mouse.[(triple1)] The cow needs the tiger.[(triple2)] The cow sees the mouse.[(triple3)] The mouse chases the cow.[(triple4)] The mouse chases the tiger.[(triple5)] The mouse needs the cow.[(triple6)] The tiger is green.[(triple7)] @1: The cow needs the cow.[(((triple2) -> rule1))]
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple5
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1