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