The lion is cold. The mouse is green. The tiger sees the mouse. If something likes the tiger then the tiger likes the mouse. If the lion is blue and the lion is green then the lion does not need the mouse. Cold things are blue. If something needs the lion then the lion does not see the mouse. If the mouse is big and the mouse does not see the tiger then the mouse needs the lion. If the lion sees the mouse then the mouse likes the lion. If something sees the lion and the lion needs the mouse then it does not need the lion. If something likes the mouse and it is not green then it is rough.
The lion is cold.
("lion" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something likes the tiger then the tiger likes the mouse.
((("something" "likes" "tiger" "+")) -> ("tiger" "likes" "mouse" "+"))
If the lion is blue and the lion is green then the lion does not need the mouse.
((("lion" "is" "blue" "+") ("lion" "is" "green" "+")) -> ("lion" "needs" "mouse" "-"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something needs the lion then the lion does not see the mouse.
((("something" "needs" "lion" "+")) -> ("lion" "sees" "mouse" "-"))
If the mouse is big and the mouse does not see the tiger then the mouse needs the lion.
((("mouse" "is" "big" "+") ("mouse" "sees" "tiger" "~")) -> ("mouse" "needs" "lion" "+"))
If the lion sees the mouse then the mouse likes the lion.
((("lion" "sees" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If something sees the lion and the lion needs the mouse then it does not need the lion.
((("something" "sees" "lion" "+") ("lion" "needs" "mouse" "+")) -> ("something" "needs" "lion" "-"))
If something likes the mouse and it is not green then it is rough.
((("something" "likes" "mouse" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "+"))
The mouse is green.
True
1
proof
[(triple2)]
("mouse" "is" "green" "+")
triple2
The mouse is not green.
False
1
inv-proof
[(triple2)]
("mouse" "is" "green" "-")
triple2
The lion is blue.
True
2
proof
[(((triple1) -> rule3))]
("lion" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("lion" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "rough" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "blue" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
@0: The lion is cold.[(triple1)] The mouse is green.[(triple2)] The tiger sees the mouse.[(triple3)] @1: The lion is blue.[(((triple1) -> rule3))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1