The bear is green. The bear is kind. The bear is round. The cow visits the mouse. The mouse chases the bear. The mouse chases the cow. The mouse visits the bear. If someone sees the cow then the cow sees the mouse. If someone chases the mouse then they see the cow. If someone chases the bear and the bear is nice then the bear is kind. If the cow visits the bear then the cow sees the bear. If someone is kind then they see the cow. If someone is rough and they visit the bear then the bear is green. If someone chases the cow then the cow is rough. If someone sees the cow and the cow chases the bear then the bear visits the cow.
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is round.
("bear" "is" "round" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone sees the cow then the cow sees the mouse.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If someone chases the mouse then they see the cow.
((("someone" "chases" "mouse" "+")) -> ("someone" "sees" "cow" "+"))
If someone chases the bear and the bear is nice then the bear is kind.
((("someone" "chases" "bear" "+") ("bear" "is" "nice" "+")) -> ("bear" "is" "kind" "+"))
If the cow visits the bear then the cow sees the bear.
((("cow" "visits" "bear" "+")) -> ("cow" "sees" "bear" "+"))
If someone is kind then they see the cow.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "cow" "+"))
If someone is rough and they visit the bear then the bear is green.
((("someone" "is" "rough" "+") ("someone" "visits" "bear" "+")) -> ("bear" "is" "green" "+"))
If someone chases the cow then the cow is rough.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "rough" "+"))
If someone sees the cow and the cow chases the bear then the bear visits the cow.
((("someone" "sees" "cow" "+") ("cow" "chases" "bear" "+")) -> ("bear" "visits" "cow" "+"))
The bear is kind.
True
1
proof
[(triple2)]
("bear" "is" "kind" "+")
triple2
The bear is not round.
False
1
inv-proof
[(triple3)]
("bear" "is" "round" "-")
triple3
The mouse does not see the cow.
Unknown
inv-rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "cow" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
@0: The bear is green.[(triple1)] The bear is kind.[(triple2)] The bear is round.[(triple3)] The cow visits the mouse.[(triple4)] The mouse chases the bear.[(triple5)] The mouse chases the cow.[(triple6)] The mouse visits the bear.[(triple7)] @1: The bear sees the cow.[(((triple2) -> rule5))] The cow is rough.[(((triple6) -> rule7))] @2: The cow sees the mouse.[(((((triple2) -> rule5)) -> rule1))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple7
The bear sees the cow.
("bear" "sees" "cow" "+")
((triple2) -> (rule5 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple6) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2