The lion eats the mouse. The lion needs the mouse. The mouse likes the lion. If someone needs the mouse and they eat the lion then they are cold. If someone is green then they like the mouse. If someone is cold then they need the lion. If someone needs the mouse then they like the mouse. If someone needs the mouse and they eat the mouse then they like the mouse. If someone likes the mouse then they are kind.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If someone needs the mouse and they eat the lion then they are cold.
((("someone" "needs" "mouse" "+") ("someone" "eats" "lion" "+")) -> ("someone" "is" "cold" "+"))
If someone is green then they like the mouse.
((("someone" "is" "green" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is cold then they need the lion.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the mouse then they like the mouse.
((("someone" "needs" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
If someone needs the mouse and they eat the mouse then they like the mouse.
((("someone" "needs" "mouse" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then they are kind.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "kind" "+"))
The lion needs the mouse.
True
1
proof
[(triple2)]
("lion" "needs" "mouse" "+")
triple2
The mouse does not like the lion.
False
1
inv-proof
[(triple3)]
("mouse" "likes" "lion" "-")
triple3
The lion likes the mouse.
True
2
proof
[(((triple2) -> rule4) OR ((triple2 triple1) -> rule5))]
("lion" "likes" "mouse" "+")
((triple2) -> (rule4 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
((triple2 triple1) -> (rule5 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion does not like the mouse.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple2 triple1) -> rule5))]
("lion" "likes" "mouse" "-")
((triple2) -> (rule4 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
((triple2 triple1) -> (rule5 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion is kind.
True
3
proof
[(((((triple2) -> rule4)) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule6))]
("lion" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
((((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion is not kind.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule6))]
("lion" "is" "kind" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
((((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse does not need the lion.
Unknown
inv-rconc
[@2: The mouse needs the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("mouse" "needs" "lion" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
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 blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion eats the mouse.[(triple1)] The lion needs the mouse.[(triple2)] The mouse likes the lion.[(triple3)] @1: The lion likes the mouse.[(((triple2) -> rule4) OR ((triple2 triple1) -> rule5))] @2: The lion is kind.[(((((triple2) -> rule4)) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule6))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((triple2) -> (rule4 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
((triple2 triple1) -> (rule5 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
((((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2