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