The lion eats the squirrel. The squirrel chases the lion. The squirrel eats the lion. If someone chases the lion then they are red. If someone sees the squirrel then they chase the lion. If the squirrel chases the lion then the lion is rough. All rough people are young. If someone eats the lion and they see the lion then they see the squirrel. If someone sees the lion and they chase the squirrel then the lion chases the squirrel. If someone chases the lion and they eat the lion then the lion chases the squirrel. If someone eats the squirrel then they see the squirrel.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If someone chases the lion then they are red.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "red" "+"))
If someone sees the squirrel then they chase the lion.
((("someone" "sees" "squirrel" "+")) -> ("someone" "chases" "lion" "+"))
If the squirrel chases the lion then the lion is rough.
((("squirrel" "chases" "lion" "+")) -> ("lion" "is" "rough" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone eats the lion and they see the lion then they see the squirrel.
((("someone" "eats" "lion" "+") ("someone" "sees" "lion" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone sees the lion and they chase the squirrel then the lion chases the squirrel.
((("someone" "sees" "lion" "+") ("someone" "chases" "squirrel" "+")) -> ("lion" "chases" "squirrel" "+"))
If someone chases the lion and they eat the lion then the lion chases the squirrel.
((("someone" "chases" "lion" "+") ("someone" "eats" "lion" "+")) -> ("lion" "chases" "squirrel" "+"))
If someone eats the squirrel then they see the squirrel.
((("someone" "eats" "squirrel" "+")) -> ("someone" "sees" "squirrel" "+"))
The lion eats the squirrel.
True
1
proof
[(triple1)]
("lion" "eats" "squirrel" "+")
triple1
The squirrel does not chase the lion.
False
1
inv-proof
[(triple2)]
("squirrel" "chases" "lion" "-")
triple2
The lion is rough.
True
2
proof
[(((triple2) -> rule3))]
("lion" "is" "rough" "+")
((triple2) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion does not chase the squirrel.
False
3
inv-proof
[(((triple2 triple3) -> rule7))]
("lion" "chases" "squirrel" "-")
((triple2 triple3) -> (rule7 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion is young.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("lion" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion does not chase the lion.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule2))]
("lion" "chases" "lion" "-")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion is red.
True
4
proof
[(((((((triple1) -> rule8)) -> rule2)) -> rule1))]
("lion" "is" "red" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The lion is not red.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule2)) -> rule1))]
("lion" "is" "red" "-")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "young" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel sees the lion.
Unknown
random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion eats the squirrel.[(triple1)] The squirrel chases the lion.[(triple2)] The squirrel eats the lion.[(triple3)] @1: The lion chases the squirrel.[(((triple2 triple3) -> rule7))] The lion is rough.[(((triple2) -> rule3))] The lion sees the squirrel.[(((triple1) -> rule8))] The squirrel is red.[(((triple2) -> rule1))] @2: The lion chases the lion.[(((((triple1) -> rule8)) -> rule2))] The lion is young.[(((((triple2) -> rule3)) -> rule4))] @3: The lion is red.[(((((((triple1) -> rule8)) -> rule2)) -> rule1))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple3
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple2 triple3) -> (rule7 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple2) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((triple1) -> (rule8 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((triple2) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3