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