The lion is blue. The lion needs the mouse. The mouse needs the lion. If something is blue and it needs the lion then the lion is cold. If something needs the lion then it is blue.
The lion is blue.
("lion" "is" "blue" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If something is blue and it needs the lion then the lion is cold.
((("something" "is" "blue" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "cold" "+"))
If something needs the lion then it is blue.
((("something" "needs" "lion" "+")) -> ("something" "is" "blue" "+"))
The mouse needs the lion.
True
1
proof
[(triple3)]
("mouse" "needs" "lion" "+")
triple3
The mouse does not need the lion.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "lion" "-")
triple3
The mouse is blue.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "is" "blue" "+")
((triple3) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "is" "blue" "-")
((triple3) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The lion is cold.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("lion" "is" "cold" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The lion is not cold.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("lion" "is" "cold" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
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 mouse chases the lion.
Unknown
random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse sees the lion.
Unknown
random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "+")
@0: The lion is blue.[(triple1)] The lion needs the mouse.[(triple2)] The mouse needs the lion.[(triple3)] @1: The mouse is blue.[(((triple3) -> rule2))] @2: The lion is cold.[(((((triple3) -> rule2) triple3) -> rule1))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
((triple3) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2