The bald eagle is kind. The bald eagle visits the lion. The cat is kind. The cat is rough. The cat does not see the lion. The lion is kind. The lion is rough. The lion visits the squirrel. The squirrel is kind. The squirrel is not round. The squirrel visits the bald eagle. The squirrel visits the lion. If someone sees the bald eagle then they see the cat. If someone is kind and they see the bald eagle then they visit the bald eagle. If the squirrel chases the lion then the lion does not chase the cat. If someone visits the lion then the lion is red. If someone visits the lion and they are red then they see the lion. If someone is red then they do not visit the lion. If someone is round and they do not see the cat then the cat sees the squirrel. If someone visits the lion and the lion does not chase the cat then the cat is round.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat does not see the lion.
("cat" "sees" "lion" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If someone sees the bald eagle then they see the cat.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "sees" "cat" "+"))
If someone is kind and they see the bald eagle then they visit the bald eagle.
((("someone" "is" "kind" "+") ("someone" "sees" "bald eagle" "+")) -> ("someone" "visits" "bald eagle" "+"))
If the squirrel chases the lion then the lion does not chase the cat.
((("squirrel" "chases" "lion" "+")) -> ("lion" "chases" "cat" "-"))
If someone visits the lion then the lion is red.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "red" "+"))
If someone visits the lion and they are red then they see the lion.
((("someone" "visits" "lion" "+") ("someone" "is" "red" "+")) -> ("someone" "sees" "lion" "+"))
If someone is red then they do not visit the lion.
((("someone" "is" "red" "+")) -> ("someone" "visits" "lion" "-"))
If someone is round and they do not see the cat then the cat sees the squirrel.
((("someone" "is" "round" "+") ("someone" "sees" "cat" "~")) -> ("cat" "sees" "squirrel" "+"))
If someone visits the lion and the lion does not chase the cat then the cat is round.
((("someone" "visits" "lion" "+") ("lion" "chases" "cat" "~")) -> ("cat" "is" "round" "+"))
The bald eagle visits the lion.
True
1
proof
[(triple2)]
("bald eagle" "visits" "lion" "+")
triple2
The cat is not rough.
False
1
inv-proof
[(triple4)]
("cat" "is" "rough" "-")
triple4
The lion is red.
True
2
proof
[(((triple12) -> rule4) OR ((triple2) -> rule4))]
("lion" "is" "red" "+")
((triple12) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple2) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple12) -> rule4) OR ((triple2) -> rule4))]
("lion" "is" "red" "-")
((triple12) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple2) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion does not visit the lion.
True
3
proof
[(((((triple12) -> rule4)) -> rule6) OR ((((triple2) -> rule4)) -> rule6))]
("lion" "visits" "lion" "-")
((((triple12) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion visits the lion.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule6) OR ((((triple2) -> rule4)) -> rule6))]
("lion" "visits" "lion" "+")
((((triple12) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion does not see the cat.
Unknown
inv-rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "cat" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "round" "+")
The squirrel does not see the lion.
Unknown
inv-rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "lion" "-")
The bald eagle is nice.
Unknown
random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The bald eagle visits the cat.
Unknown
random
[@0: The bald eagle visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "cat" "+")
@0: The bald eagle is kind.[(triple1)] The bald eagle visits the lion.[(triple2)] The cat does not see the lion.[(triple5)] The cat is kind.[(triple3)] The cat is rough.[(triple4)] The lion is kind.[(triple6)] The lion is rough.[(triple7)] The lion visits the squirrel.[(triple8)] The squirrel is kind.[(triple9)] The squirrel is not round.[(triple10)] The squirrel visits the bald eagle.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The lion is red.[(((triple12) -> rule4) OR ((triple2) -> rule4))] @2: The lion does not visit the lion.[(((((triple12) -> rule4)) -> rule6) OR ((((triple2) -> rule4)) -> rule6))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
triple2
The cat does not see the lion.
("cat" "sees" "lion" "-")
triple5
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel is not round.
("squirrel" "is" "round" "-")
triple10
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The lion is red.
("lion" "is" "red" "+")
((triple12) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple2) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion does not visit the lion.
("lion" "visits" "lion" "-")
((((triple12) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2