The lion chases the squirrel. The lion is green. The lion is red. The squirrel sees the tiger. The tiger chases the lion. The tiger chases the squirrel. The tiger sees the lion. If something needs the lion then it needs the squirrel. If something chases the squirrel and the squirrel sees the tiger then it needs the lion.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something needs the lion then it needs the squirrel.
((("something" "needs" "lion" "+")) -> ("something" "needs" "squirrel" "+"))
If something chases the squirrel and the squirrel sees the tiger then it needs the lion.
((("something" "chases" "squirrel" "+") ("squirrel" "sees" "tiger" "+")) -> ("something" "needs" "lion" "+"))
The lion is green.
True
1
proof
[(triple2)]
("lion" "is" "green" "+")
triple2
The tiger does not see the lion.
False
1
inv-proof
[(triple7)]
("tiger" "sees" "lion" "-")
triple7
The tiger needs the lion.
True
3
proof
[(((triple6 triple4) -> rule2))]
("tiger" "needs" "lion" "+")
((triple6 triple4) -> (rule2 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger does not need the lion.
False
3
inv-proof
[(((triple6 triple4) -> rule2))]
("tiger" "needs" "lion" "-")
((triple6 triple4) -> (rule2 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the squirrel.
True
4
proof
[(((((triple6 triple4) -> rule2)) -> rule1))]
("tiger" "needs" "squirrel" "+")
((((triple6 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion does not need the squirrel.
False
4
inv-proof
[(((((triple1 triple4) -> rule2)) -> rule1))]
("lion" "needs" "squirrel" "-")
((((triple1 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The squirrel does not need the lion.
Unknown
inv-rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "lion" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@2: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
@0: The lion chases the squirrel.[(triple1)] The lion is green.[(triple2)] The lion is red.[(triple3)] The squirrel sees the tiger.[(triple4)] The tiger chases the lion.[(triple5)] The tiger chases the squirrel.[(triple6)] The tiger sees the lion.[(triple7)] @1: The lion needs the lion.[(((triple1 triple4) -> rule2))] The tiger needs the lion.[(((triple6 triple4) -> rule2))] @2: The lion needs the squirrel.[(((((triple1 triple4) -> rule2)) -> rule1))] The tiger needs the squirrel.[(((((triple6 triple4) -> rule2)) -> rule1))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple4
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple5
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple1 triple4) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((triple6 triple4) -> (rule2 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((((triple1 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
((((triple6 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2