The cow chases the mouse. The cow is big. The cow likes the mouse. The cow sees the mouse. The mouse is green. The mouse is kind. The mouse sees the cow. If something sees the mouse and it is green then it likes the cow. If something chases the cow then it likes the mouse. If something chases the mouse and it likes the mouse then the mouse sees the cow. If the cow likes the mouse then the mouse likes the cow. If something likes the cow then it is green. If something chases the cow and the cow is big then it likes the mouse.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something sees the mouse and it is green then it likes the cow.
((("something" "sees" "mouse" "+") ("something" "is" "green" "+")) -> ("something" "likes" "cow" "+"))
If something chases the cow then it likes the mouse.
((("something" "chases" "cow" "+")) -> ("something" "likes" "mouse" "+"))
If something chases the mouse and it likes the mouse then the mouse sees the cow.
((("something" "chases" "mouse" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If the cow likes the mouse then the mouse likes the cow.
((("cow" "likes" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If something likes the cow then it is green.
((("something" "likes" "cow" "+")) -> ("something" "is" "green" "+"))
If something chases the cow and the cow is big then it likes the mouse.
((("something" "chases" "cow" "+") ("cow" "is" "big" "+")) -> ("something" "likes" "mouse" "+"))
The cow likes the mouse.
True
1
proof
[(triple3)]
("cow" "likes" "mouse" "+")
triple3
The mouse does not see the cow.
False
1
inv-proof
[(triple7 OR ((triple1 triple3) -> rule3))]
("mouse" "sees" "cow" "-")
triple7
((triple1 triple3) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "likes" "cow" "+")
((triple3) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse does not like the cow.
False
2
inv-proof
[(((triple3) -> rule4))]
("mouse" "likes" "cow" "-")
((triple3) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow does not like the cow.
Unknown
inv-rconc
[@2: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("cow" "likes" "cow" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cow chases the mouse.[(triple1)] The cow is big.[(triple2)] The cow likes the mouse.[(triple3)] The cow sees the mouse.[(triple4)] The mouse is green.[(triple5 OR ((((triple3) -> rule4)) -> rule5))] The mouse is kind.[(triple6)] The mouse sees the cow.[(triple7 OR ((triple1 triple3) -> rule3))] @1: The mouse likes the cow.[(((triple3) -> rule4))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
((triple1 triple3) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((triple3) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1