The bear eats the mouse. The bear needs the tiger. The mouse is cold. The mouse needs the bear. The tiger eats the bear. The tiger is cold. The tiger needs the mouse. If the tiger likes the bear and the tiger is not nice then the tiger needs the mouse. If something likes the bear then it is rough. If something needs the tiger then the tiger likes the bear.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If the tiger likes the bear and the tiger is not nice then the tiger needs the mouse.
((("tiger" "likes" "bear" "+") ("tiger" "is" "nice" "~")) -> ("tiger" "needs" "mouse" "+"))
If something likes the bear then it is rough.
((("something" "likes" "bear" "+")) -> ("something" "is" "rough" "+"))
If something needs the tiger then the tiger likes the bear.
((("something" "needs" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
The tiger needs the mouse.
True
1
proof
[(triple7)]
("tiger" "needs" "mouse" "+")
triple7
The tiger does not need the mouse.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "mouse" "-")
triple7
The tiger likes the bear.
True
2
proof
[(((triple2) -> rule3))]
("tiger" "likes" "bear" "+")
((triple2) -> (rule3 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger does not like the bear.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "likes" "bear" "-")
((triple2) -> (rule3 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger is rough.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("tiger" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger is not rough.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("tiger" "is" "rough" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "rough" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "rough" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The bear eats the mouse.[(triple1)] The bear needs the tiger.[(triple2)] The mouse is cold.[(triple3)] The mouse needs the bear.[(triple4)] The tiger eats the bear.[(triple5)] The tiger is cold.[(triple6)] The tiger needs the mouse.[(triple7)] @1: The tiger likes the bear.[(((triple2) -> rule3))] @2: The tiger is rough.[(((((triple2) -> rule3)) -> rule2))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple4
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple7
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((triple2) -> (rule3 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2