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