The bear is red. The bear is round. The bear sees the mouse. The bear visits the mouse. The mouse is kind. The mouse sees the bear. The mouse visits the bear. If the bear sees the mouse and the mouse visits the bear then the mouse eats the bear. Rough things are blue.
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If the bear sees the mouse and the mouse visits the bear then the mouse eats the bear.
((("bear" "sees" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("mouse" "eats" "bear" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
The bear sees the mouse.
True
1
proof
[(triple3)]
("bear" "sees" "mouse" "+")
triple3
The mouse does not see the bear.
False
1
inv-proof
[(triple6)]
("mouse" "sees" "bear" "-")
triple6
The mouse eats the bear.
True
3
proof
[(((triple3 triple7) -> rule1))]
("mouse" "eats" "bear" "+")
((triple3 triple7) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not eat the bear.
False
3
inv-proof
[(((triple3 triple7) -> rule1))]
("mouse" "eats" "bear" "-")
((triple3 triple7) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "blue" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "blue" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bear is red.[(triple1)] The bear is round.[(triple2)] The bear sees the mouse.[(triple3)] The bear visits the mouse.[(triple4)] The mouse is kind.[(triple5)] The mouse sees the bear.[(triple6)] The mouse visits the bear.[(triple7)] @1: The mouse eats the bear.[(((triple3 triple7) -> rule1))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple6
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple7
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple3 triple7) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1