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