The bear is young. The mouse chases the tiger. The mouse needs the bear. The mouse sees the bear. The mouse sees the tiger. The tiger is blue. The tiger is cold. The tiger is kind. The tiger needs the mouse. The tiger sees the bear. If something is nice then it is blue. If something needs the bear then it sees the mouse.
The bear is young.
("bear" "is" "young" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something needs the bear then it sees the mouse.
((("something" "needs" "bear" "+")) -> ("something" "sees" "mouse" "+"))
The mouse sees the tiger.
True
1
proof
[(triple5)]
("mouse" "sees" "tiger" "+")
triple5
The tiger does not need the mouse.
False
1
inv-proof
[(triple9)]
("tiger" "needs" "mouse" "-")
triple9
The mouse sees the mouse.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "sees" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "sees" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The bear does not see the mouse.
Unknown
inv-rconc
[@1: The bear sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "mouse" "-")
The tiger sees the mouse.
Unknown
rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "mouse" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The tiger chases the mouse.
Unknown
random
[@0: The tiger chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "mouse" "+")
@0: The bear is young.[(triple1)] The mouse chases the tiger.[(triple2)] The mouse needs the bear.[(triple3)] The mouse sees the bear.[(triple4)] The mouse sees the tiger.[(triple5)] The tiger is blue.[(triple6)] The tiger is cold.[(triple7)] The tiger is kind.[(triple8)] The tiger needs the mouse.[(triple9)] The tiger sees the bear.[(triple10)] @1: The mouse sees the mouse.[(((triple3) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple3
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple9
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple10
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1