The lion eats the mouse. The lion is blue. The lion does not need the mouse. The mouse does not eat the lion. The mouse needs the lion. The mouse does not visit the tiger. The tiger is not cold. The tiger is not kind. The tiger visits the lion. The tiger visits the mouse. If something needs the lion and it does not visit the tiger then it is blue. If something is nice then it does not eat the tiger. If something is nice then it visits the lion.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
The mouse does not eat the lion.
("mouse" "eats" "lion" "-")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something needs the lion and it does not visit the tiger then it is blue.
((("something" "needs" "lion" "+") ("something" "visits" "tiger" "~")) -> ("something" "is" "blue" "+"))
If something is nice then it does not eat the tiger.
((("something" "is" "nice" "+")) -> ("something" "eats" "tiger" "-"))
If something is nice then it visits the lion.
((("something" "is" "nice" "+")) -> ("something" "visits" "lion" "+"))
The mouse does not eat the lion.
True
1
proof
[(triple4)]
("mouse" "eats" "lion" "-")
triple4
The mouse eats the lion.
False
1
inv-proof
[(triple4)]
("mouse" "eats" "lion" "+")
triple4
The mouse is blue.
True
3
proof
[(((triple5 triple6) -> rule1))]
("mouse" "is" "blue" "+")
((triple5 triple6) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is not blue.
False
3
inv-proof
[(((triple5 triple6) -> rule1))]
("mouse" "is" "blue" "-")
((triple5 triple6) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "blue" "-")
The mouse visits the lion.
Unknown
rconc
[@1: The mouse visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "lion" "+")
The lion does not need the tiger.
Unknown
inv-random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The lion does not need the mouse.[(triple3)] The lion eats the mouse.[(triple1)] The lion is blue.[(triple2)] The mouse does not eat the lion.[(triple4)] The mouse does not visit the tiger.[(triple6)] The mouse needs the lion.[(triple5)] The tiger is not cold.[(triple7)] The tiger is not kind.[(triple8)] The tiger visits the lion.[(triple9)] The tiger visits the mouse.[(triple10)] @1: The mouse is blue.[(((triple5 triple6) -> rule1))]
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
triple3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The mouse does not eat the lion.
("mouse" "eats" "lion" "-")
triple4
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
triple6
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple5
The tiger is not cold.
("tiger" "is" "cold" "-")
triple7
The tiger is not kind.
("tiger" "is" "kind" "-")
triple8
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple9
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple10
The mouse is blue.
("mouse" "is" "blue" "+")
((triple5 triple6) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1