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