The lion is blue. The lion is green. The lion is not kind. The lion needs the mouse. The lion sees the mouse. The lion visits the mouse. The mouse is nice. The mouse is red. The mouse needs the lion. The mouse visits the lion. If someone is red and they need the mouse then the mouse does not see the lion. If someone is green then they see the lion. If someone visits the mouse then the mouse is green.
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone is red and they need the mouse then the mouse does not see the lion.
((("someone" "is" "red" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "lion" "-"))
If someone is green then they see the lion.
((("someone" "is" "green" "+")) -> ("someone" "sees" "lion" "+"))
If someone visits the mouse then the mouse is green.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "green" "+"))
The lion needs the mouse.
True
1
proof
[(triple4)]
("lion" "needs" "mouse" "+")
triple4
The mouse does not visit the lion.
False
1
inv-proof
[(triple10)]
("mouse" "visits" "lion" "-")
triple10
The lion sees the lion.
True
2
proof
[(((triple2) -> rule2))]
("lion" "sees" "lion" "+")
((triple2) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple2) -> rule2))]
("lion" "sees" "lion" "-")
((triple2) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The mouse sees the lion.
True
3
proof
[(((((triple6) -> rule3)) -> rule2))]
("mouse" "sees" "lion" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse does not see the lion.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule2))]
("mouse" "sees" "lion" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The lion is blue.[(triple1)] The lion is green.[(triple2)] The lion is not kind.[(triple3)] The lion needs the mouse.[(triple4)] The lion sees the mouse.[(triple5)] The lion visits the mouse.[(triple6)] The mouse is nice.[(triple7)] The mouse is red.[(triple8)] The mouse needs the lion.[(triple9)] The mouse visits the lion.[(triple10)] @1: The lion sees the lion.[(((triple2) -> rule2))] The mouse is green.[(((triple6) -> rule3))] @2: The mouse sees the lion.[(((((triple6) -> rule3)) -> rule2))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is not kind.
("lion" "is" "kind" "-")
triple3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple5
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple6
The mouse is nice.
("mouse" "is" "nice" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
triple8
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple2) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((triple6) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2