The lion chases the squirrel. The lion is not big. The lion sees the squirrel. The lion sees the tiger. The lion does not visit the tiger. The squirrel chases the lion. The squirrel chases the tiger. The squirrel is cold. The squirrel sees the lion. The squirrel does not visit the lion. The squirrel visits the tiger. The tiger chases the lion. The tiger is rough. The tiger sees the lion. The tiger visits the lion. The tiger does not visit the squirrel. If someone visits the lion and the lion is not rough then the lion visits the squirrel. If someone is rough and blue then they chase the squirrel. If someone visits the tiger then they are nice. If someone visits the tiger then the tiger visits the lion. If someone sees the lion and the lion visits the tiger then the lion does not see the squirrel. If someone chases the squirrel and they do not see the tiger then the tiger does not see the lion. If the lion sees the squirrel then the squirrel is nice. If someone sees the tiger and they do not visit the squirrel then they chase the tiger.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
If someone visits the lion and the lion is not rough then the lion visits the squirrel.
((("someone" "visits" "lion" "+") ("lion" "is" "rough" "~")) -> ("lion" "visits" "squirrel" "+"))
If someone is rough and blue then they chase the squirrel.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone visits the tiger then they are nice.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the tiger then the tiger visits the lion.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If someone sees the lion and the lion visits the tiger then the lion does not see the squirrel.
((("someone" "sees" "lion" "+") ("lion" "visits" "tiger" "+")) -> ("lion" "sees" "squirrel" "-"))
If someone chases the squirrel and they do not see the tiger then the tiger does not see the lion.
((("someone" "chases" "squirrel" "+") ("someone" "sees" "tiger" "~")) -> ("tiger" "sees" "lion" "-"))
If the lion sees the squirrel then the squirrel is nice.
((("lion" "sees" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If someone sees the tiger and they do not visit the squirrel then they chase the tiger.
((("someone" "sees" "tiger" "+") ("someone" "visits" "squirrel" "~")) -> ("someone" "chases" "tiger" "+"))
The lion is not big.
True
1
proof
[(triple2)]
("lion" "is" "big" "-")
triple2
The tiger does not see the lion.
False
1
inv-proof
[(triple14)]
("tiger" "sees" "lion" "-")
triple14
The squirrel is nice.
True
2
proof
[(((triple11) -> rule3) OR ((triple3) -> rule7))]
("squirrel" "is" "nice" "+")
((triple11) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule7 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple11) -> rule3) OR ((triple3) -> rule7))]
("squirrel" "is" "nice" "-")
((triple11) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule7 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "nice" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion chases the squirrel.[(triple1)] The lion does not visit the tiger.[(triple5)] The lion is not big.[(triple2)] The lion sees the squirrel.[(triple3)] The lion sees the tiger.[(triple4)] The squirrel chases the lion.[(triple6)] The squirrel chases the tiger.[(triple7)] The squirrel does not visit the lion.[(triple10)] The squirrel is cold.[(triple8)] The squirrel sees the lion.[(triple9)] The squirrel visits the tiger.[(triple11)] The tiger chases the lion.[(triple12)] The tiger does not visit the squirrel.[(triple16)] The tiger is rough.[(triple13)] The tiger sees the lion.[(triple14)] The tiger visits the lion.[(triple15 OR ((triple11) -> rule4))] @1: The squirrel is nice.[(((triple11) -> rule3) OR ((triple3) -> rule7))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
triple5
The lion is not big.
("lion" "is" "big" "-")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple6
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple7
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple11
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple12
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
triple16
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
((triple11) -> (rule4 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple11) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple3) -> (rule7 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1