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