The lion is blue. The lion is kind. The lion is nice. The lion is rough. The lion is young. The lion likes the squirrel. The lion sees the squirrel. The lion visits the squirrel. The squirrel is blue. The squirrel is kind. The squirrel is nice. The squirrel is rough. The squirrel is young. The squirrel likes the lion. The squirrel sees the lion. The squirrel visits the lion. If someone visits the squirrel and the squirrel sees the lion then the lion sees the squirrel. If someone sees the squirrel then the squirrel sees the lion. If the lion likes the squirrel then the squirrel likes the lion. If someone likes the lion then they visit the squirrel. If someone is young and rough then they visit the squirrel. If someone sees the lion then they visit 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 rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes 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 kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If someone visits the squirrel and the squirrel sees the lion then the lion sees the squirrel.
((("someone" "visits" "squirrel" "+") ("squirrel" "sees" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If someone sees the squirrel then the squirrel sees the lion.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If the lion likes the squirrel then the squirrel likes the lion.
((("lion" "likes" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If someone likes the lion then they visit the squirrel.
((("someone" "likes" "lion" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is young and rough then they visit the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone sees the lion then they visit the lion.
((("someone" "sees" "lion" "+")) -> ("someone" "visits" "lion" "+"))
The lion is rough.
True
1
proof
[(triple4)]
("lion" "is" "rough" "+")
triple4
The squirrel does not visit the lion.
False
1
inv-proof
[(triple16 OR ((triple15) -> rule6) OR ((((triple7) -> rule2)) -> rule6))]
("squirrel" "visits" "lion" "-")
triple16
((triple15) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel visits the squirrel.
True
2
proof
[(((triple14) -> rule4) OR ((triple13 triple12) -> rule5) OR ((((triple6) -> rule3)) -> rule4))]
("squirrel" "visits" "squirrel" "+")
((triple14) -> (rule4 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((triple13 triple12) -> (rule5 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple14) -> rule4) OR ((triple13 triple12) -> rule5) OR ((((triple6) -> rule3)) -> rule4))]
("squirrel" "visits" "squirrel" "-")
((triple14) -> (rule4 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((triple13 triple12) -> (rule5 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The lion is blue.[(triple1)] The lion is kind.[(triple2)] The lion is nice.[(triple3)] The lion is rough.[(triple4)] The lion is young.[(triple5)] The lion likes the squirrel.[(triple6)] The lion sees the squirrel.[(triple7 OR ((triple8 triple15) -> rule1) OR ((((triple14) -> rule4) triple15) -> rule1) OR ((((triple13 triple12) -> rule5) triple15) -> rule1) OR ((((triple5 triple4) -> rule5) triple15) -> rule1) OR ((((((triple6) -> rule3)) -> rule4) triple15) -> rule1))] The lion visits the squirrel.[(triple8 OR ((triple5 triple4) -> rule5))] The squirrel is blue.[(triple9)] The squirrel is kind.[(triple10)] The squirrel is nice.[(triple11)] The squirrel is rough.[(triple12)] The squirrel is young.[(triple13)] The squirrel likes the lion.[(triple14 OR ((triple6) -> rule3))] The squirrel sees the lion.[(triple15 OR ((triple7) -> rule2))] The squirrel visits the lion.[(triple16 OR ((triple15) -> rule6) OR ((((triple7) -> rule2)) -> rule6))] @1: The squirrel visits the squirrel.[(((triple14) -> rule4) OR ((triple13 triple12) -> rule5) OR ((((triple6) -> rule3)) -> rule4))]
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 rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple6
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple7
((triple8 triple15) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
((((triple14) -> (rule4 % int2)) triple15) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
((((triple13 triple12) -> (rule5 % int2)) triple15) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
((((triple5 triple4) -> (rule5 % int2)) triple15) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2)) triple15) -> (rule1 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
((triple5 triple4) -> (rule5 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple11
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple12
The squirrel is young.
("squirrel" "is" "young" "+")
triple13
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple14
((triple6) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple15
((triple7) -> (rule2 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple16
((triple15) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple14) -> (rule4 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((triple13 triple12) -> (rule5 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2