The bear needs the squirrel. The lion chases the bear. The squirrel chases the lion. If something visits the lion then it visits the squirrel. If something needs the squirrel then the squirrel visits the lion.
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
If something visits the lion then it visits the squirrel.
((("something" "visits" "lion" "+")) -> ("something" "visits" "squirrel" "+"))
If something needs the squirrel then the squirrel visits the lion.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "visits" "lion" "+"))
The lion chases the bear.
True
1
proof
[(triple2)]
("lion" "chases" "bear" "+")
triple2
The bear does not need the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "needs" "squirrel" "-")
triple1
The squirrel visits the lion.
True
2
proof
[(((triple1) -> rule2))]
("squirrel" "visits" "lion" "+")
((triple1) -> (rule2 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule2))]
("squirrel" "visits" "lion" "-")
((triple1) -> (rule2 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel visits the squirrel.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("squirrel" "visits" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel does not visit the squirrel.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("squirrel" "visits" "squirrel" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The lion does not visit the squirrel.
Unknown
inv-rconc
[@1: The lion visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "squirrel" "-")
The bear visits the squirrel.
Unknown
rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "squirrel" "+")
The bear does not chase the squirrel.
Unknown
inv-random
[@0: The bear chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "squirrel" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
@0: The bear needs the squirrel.[(triple1)] The lion chases the bear.[(triple2)] The squirrel chases the lion.[(triple3)] @1: The squirrel visits the lion.[(((triple1) -> rule2))] @2: The squirrel visits the squirrel.[(((((triple1) -> rule2)) -> rule1))]
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple1
The lion chases the bear.
("lion" "chases" "bear" "+")
triple2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple3
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((triple1) -> (rule2 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2