The lion is young. The squirrel chases the lion. The squirrel eats the lion. If someone is cold then they visit the lion. If someone visits the lion and they eat the lion then the lion is young. If the lion eats the squirrel then the lion chases the squirrel. If someone is round and they chase the squirrel then the squirrel visits the lion. If someone is round then they chase the squirrel. If the lion eats the squirrel then the lion chases the squirrel. Cold, young people are nice. If someone is young then they eat the squirrel.
The lion is young.
("lion" "is" "young" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If someone is cold then they visit the lion.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the lion and they eat the lion then the lion is young.
((("someone" "visits" "lion" "+") ("someone" "eats" "lion" "+")) -> ("lion" "is" "young" "+"))
If the lion eats the squirrel then the lion chases the squirrel.
((("lion" "eats" "squirrel" "+")) -> ("lion" "chases" "squirrel" "+"))
If someone is round and they chase the squirrel then the squirrel visits the lion.
((("someone" "is" "round" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "visits" "lion" "+"))
If someone is round then they chase the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "chases" "squirrel" "+"))
If the lion eats the squirrel then the lion chases the squirrel.
((("lion" "eats" "squirrel" "+")) -> ("lion" "chases" "squirrel" "+"))
Cold, young people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they eat the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "eats" "squirrel" "+"))
The lion is young.
True
1
proof
[(triple1)]
("lion" "is" "young" "+")
triple1
The squirrel does not chase the lion.
False
1
inv-proof
[(triple2)]
("squirrel" "chases" "lion" "-")
triple2
The lion eats the squirrel.
True
2
proof
[(((triple1) -> rule8))]
("lion" "eats" "squirrel" "+")
((triple1) -> (rule8 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule8))]
("lion" "eats" "squirrel" "-")
((triple1) -> (rule8 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
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 lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "nice" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The lion is young.[(triple1)] The squirrel chases the lion.[(triple2)] The squirrel eats the lion.[(triple3)] @1: The lion eats the squirrel.[(((triple1) -> rule8))] @2: The lion chases the squirrel.[(((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8)) -> rule6))]
The lion is young.
("lion" "is" "young" "+")
triple1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((triple1) -> (rule8 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2