The lion chases the squirrel. The squirrel sees the lion. The tiger is green. If the tiger is blue and the tiger sees the lion then the lion is big. If something chases the tiger then the tiger needs the lion. If something chases the squirrel then it sees the squirrel.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger is green.
("tiger" "is" "green" "+")
If the tiger is blue and the tiger sees the lion then the lion is big.
((("tiger" "is" "blue" "+") ("tiger" "sees" "lion" "+")) -> ("lion" "is" "big" "+"))
If something chases the tiger then the tiger needs the lion.
((("something" "chases" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If something chases the squirrel then it sees the squirrel.
((("something" "chases" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
The lion chases the squirrel.
True
1
proof
[(triple1)]
("lion" "chases" "squirrel" "+")
triple1
The lion does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("lion" "chases" "squirrel" "-")
triple1
The lion sees the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("lion" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule3))]
("lion" "sees" "squirrel" "-")
((triple1) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The lion is big.
Unknown
rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "big" "+")
The lion does not chase the tiger.
Unknown
inv-random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The lion chases the squirrel.[(triple1)] The squirrel sees the lion.[(triple2)] The tiger is green.[(triple3)] @1: The lion sees the squirrel.[(((triple1) -> rule3))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple2
The tiger is green.
("tiger" "is" "green" "+")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1