The bear chases the mouse. The lion needs the bear. The mouse likes the bear. If someone chases the mouse then they need the lion. If someone likes the lion then they need the lion. If someone chases the mouse then the mouse likes the lion.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If someone chases the mouse then they need the lion.
((("someone" "chases" "mouse" "+")) -> ("someone" "needs" "lion" "+"))
If someone likes the lion then they need the lion.
((("someone" "likes" "lion" "+")) -> ("someone" "needs" "lion" "+"))
If someone chases the mouse then the mouse likes the lion.
((("someone" "chases" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
The bear chases the mouse.
True
1
proof
[(triple1)]
("bear" "chases" "mouse" "+")
triple1
The lion does not need the bear.
False
1
inv-proof
[(triple2)]
("lion" "needs" "bear" "-")
triple2
The mouse likes the lion.
True
2
proof
[(((triple1) -> rule3))]
("mouse" "likes" "lion" "+")
((triple1) -> (rule3 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "needs" "lion" "-")
((triple1) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The mouse needs the lion.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("mouse" "needs" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("mouse" "needs" "lion" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "lion" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The lion needs the bear.[(triple2)] The mouse likes the bear.[(triple3)] @1: The bear needs the lion.[(((triple1) -> rule1))] The mouse likes the lion.[(((triple1) -> rule3))] @2: The mouse needs the lion.[(((((triple1) -> rule3)) -> rule2))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The lion needs the bear.
("lion" "needs" "bear" "+")
triple2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple3
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple1) -> (rule3 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2