The bear is cold. The cow sees the bear. The mouse is young. If someone eats the bear and the bear is blue then the bear sees the cow. If someone is cold then they see the cow. If someone is cold and big then they see the cow. If someone is red and they eat the bear then the bear visits the mouse. If the mouse is red then the mouse visits the cow. If someone visits the mouse then they see the cow.
The bear is cold.
("bear" "is" "cold" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone eats the bear and the bear is blue then the bear sees the cow.
((("someone" "eats" "bear" "+") ("bear" "is" "blue" "+")) -> ("bear" "sees" "cow" "+"))
If someone is cold then they see the cow.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "cow" "+"))
If someone is cold and big then they see the cow.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "sees" "cow" "+"))
If someone is red and they eat the bear then the bear visits the mouse.
((("someone" "is" "red" "+") ("someone" "eats" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If the mouse is red then the mouse visits the cow.
((("mouse" "is" "red" "+")) -> ("mouse" "visits" "cow" "+"))
If someone visits the mouse then they see the cow.
((("someone" "visits" "mouse" "+")) -> ("someone" "sees" "cow" "+"))
The cow sees the bear.
True
1
proof
[(triple2)]
("cow" "sees" "bear" "+")
triple2
The mouse is not young.
False
1
inv-proof
[(triple3)]
("mouse" "is" "young" "-")
triple3
The bear sees the cow.
True
2
proof
[(((triple1) -> rule2))]
("bear" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear does not see the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "sees" "cow" "-")
((triple1) -> (rule2 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The mouse does not visit the cow.
Unknown
inv-rconc
[@1: The mouse visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "cow" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "cow" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The bear is cold.[(triple1)] The cow sees the bear.[(triple2)] The mouse is young.[(triple3)] @1: The bear sees the cow.[(((triple1) -> rule2))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The bear sees the cow.
("bear" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1