The bear likes the mouse. The lion chases the bear. The mouse likes the bear. If someone is nice and they need the mouse then the mouse is not young. If the mouse is not rough then the mouse does not need the lion. If someone is rough then they need the mouse. If someone chases the bear then they are young. If the bear likes the mouse and the bear needs the lion then the mouse likes the bear. If someone is rough and they do not chase the mouse then the mouse is big. All young people are nice. If someone likes the mouse then the mouse needs the bear.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If someone is nice and they need the mouse then the mouse is not young.
((("someone" "is" "nice" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "is" "young" "-"))
If the mouse is not rough then the mouse does not need the lion.
((("mouse" "is" "rough" "~")) -> ("mouse" "needs" "lion" "-"))
If someone is rough then they need the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "+"))
If someone chases the bear then they are young.
((("someone" "chases" "bear" "+")) -> ("someone" "is" "young" "+"))
If the bear likes the mouse and the bear needs the lion then the mouse likes the bear.
((("bear" "likes" "mouse" "+") ("bear" "needs" "lion" "+")) -> ("mouse" "likes" "bear" "+"))
If someone is rough and they do not chase the mouse then the mouse is big.
((("someone" "is" "rough" "+") ("someone" "chases" "mouse" "~")) -> ("mouse" "is" "big" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the mouse then the mouse needs the bear.
((("someone" "likes" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
The mouse likes the bear.
True
1
proof
[(triple3)]
("mouse" "likes" "bear" "+")
triple3
The lion does not chase the bear.
False
1
inv-proof
[(triple2)]
("lion" "chases" "bear" "-")
triple2
The lion is young.
True
2
proof
[(((triple2) -> rule4))]
("lion" "is" "young" "+")
((triple2) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "is" "young" "-")
((triple2) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is nice.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("lion" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("lion" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bear does not need the mouse.
Unknown
inv-rconc
[@1: The bear needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "mouse" "-")
The mouse is nice.
Unknown
rconc
[@2: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("mouse" "is" "nice" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "big" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The lion chases the mouse.
Unknown
random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "+")
@0: The bear likes the mouse.[(triple1)] The lion chases the bear.[(triple2)] The mouse likes the bear.[(triple3)] @1: The lion is young.[(((triple2) -> rule4))] The mouse needs the bear.[(((triple1) -> rule8))] @2: The lion is nice.[(((((triple2) -> rule4)) -> rule7))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The lion chases the bear.
("lion" "chases" "bear" "+")
triple2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
((triple2) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple1) -> (rule8 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2