The bear is nice. The bear needs the tiger. The cow visits the bear. The mouse is cold. The mouse is green. The mouse is red. The tiger is not cold. The tiger needs the mouse. The tiger sees the cow. The tiger does not see the mouse. If someone sees the mouse then they need the tiger. If someone sees the tiger then they are green. If someone sees the cow and they visit the mouse then the cow sees the bear. If someone needs the mouse then the mouse needs the bear. If the tiger is green then the tiger visits the mouse. If the bear does not see the mouse then the bear needs the mouse.
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
If someone sees the mouse then they need the tiger.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "tiger" "+"))
If someone sees the tiger then they are green.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "green" "+"))
If someone sees the cow and they visit the mouse then the cow sees the bear.
((("someone" "sees" "cow" "+") ("someone" "visits" "mouse" "+")) -> ("cow" "sees" "bear" "+"))
If someone needs the mouse then the mouse needs the bear.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If the tiger is green then the tiger visits the mouse.
((("tiger" "is" "green" "+")) -> ("tiger" "visits" "mouse" "+"))
If the bear does not see the mouse then the bear needs the mouse.
((("bear" "sees" "mouse" "~")) -> ("bear" "needs" "mouse" "+"))
The cow visits the bear.
True
1
proof
[(triple3)]
("cow" "visits" "bear" "+")
triple3
The mouse is not green.
False
1
inv-proof
[(triple5)]
("mouse" "is" "green" "-")
triple5
The mouse needs the bear.
True
2
proof
[(((triple8) -> rule4))]
("mouse" "needs" "bear" "+")
((triple8) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not need the bear.
False
2
inv-proof
[(((triple8) -> rule4))]
("mouse" "needs" "bear" "-")
((triple8) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger visits the mouse.
Unknown
rconc
[@2: The tiger visits the mouse.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("tiger" "visits" "mouse" "+")
The bear does not see the cow.
Unknown
inv-random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The bear is nice.[(triple1)] The bear needs the tiger.[(triple2)] The cow visits the bear.[(triple3)] The mouse is cold.[(triple4)] The mouse is green.[(triple5)] The mouse is red.[(triple6)] The tiger does not see the mouse.[(triple10)] The tiger is not cold.[(triple7)] The tiger needs the mouse.[(triple8)] The tiger sees the cow.[(triple9)] @1: The mouse needs the bear.[(((triple8) -> rule4))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The cow visits the bear.
("cow" "visits" "bear" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
triple10
The tiger is not cold.
("tiger" "is" "cold" "-")
triple7
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple8
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple9
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple8) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1