The bear likes the squirrel. The cat sees the lion. The lion sees the squirrel. The squirrel sees the bear. If someone sees the squirrel then they chase the cat. If someone chases the cat then the cat sees the squirrel.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone sees the squirrel then they chase the cat.
((("someone" "sees" "squirrel" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat then the cat sees the squirrel.
((("someone" "chases" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
The squirrel sees the bear.
True
1
proof
[(triple4)]
("squirrel" "sees" "bear" "+")
triple4
The cat does not see the lion.
False
1
inv-proof
[(triple2)]
("cat" "sees" "lion" "-")
triple2
The lion chases the cat.
True
2
proof
[(((triple3) -> rule1))]
("lion" "chases" "cat" "+")
((triple3) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion does not chase the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "chases" "cat" "-")
((triple3) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The cat sees the squirrel.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("cat" "sees" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cat does not see the squirrel.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("cat" "sees" "squirrel" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cat chases the cat.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule1))]
("cat" "chases" "cat" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The cat does not chase the cat.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule1))]
("cat" "chases" "cat" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The bear does not chase the cat.
Unknown
inv-rconc
[@1: The bear chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "cat" "-")
The squirrel chases the cat.
Unknown
rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "cat" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The bear likes the cat.
Unknown
random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "+")
The lion does not like the squirrel.
Unknown
inv-random
[@0: The lion likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "squirrel" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
The bear does not chase the lion.
Unknown
inv-random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "-")
The squirrel likes the lion.
Unknown
random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "+")
@0: The bear likes the squirrel.[(triple1)] The cat sees the lion.[(triple2)] The lion sees the squirrel.[(triple3)] The squirrel sees the bear.[(triple4)] @1: The lion chases the cat.[(((triple3) -> rule1))] @2: The cat sees the squirrel.[(((((triple3) -> rule1)) -> rule2))] @3: The cat chases the cat.[(((((((triple3) -> rule1)) -> rule2)) -> rule1))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple4
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple3) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3