The bear chases the lion. The lion is young. The lion sees the bear. If something chases the lion and the lion chases the bear then the bear sees the lion. If the bear chases the lion and the lion sees the bear then the lion chases the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If something chases the lion and the lion chases the bear then the bear sees the lion.
((("something" "chases" "lion" "+") ("lion" "chases" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If the bear chases the lion and the lion sees the bear then the lion chases the bear.
((("bear" "chases" "lion" "+") ("lion" "sees" "bear" "+")) -> ("lion" "chases" "bear" "+"))
The lion sees the bear.
True
1
proof
[(triple3)]
("lion" "sees" "bear" "+")
triple3
The bear does not chase the lion.
False
1
inv-proof
[(triple1)]
("bear" "chases" "lion" "-")
triple1
The lion chases the bear.
True
3
proof
[(((triple1 triple3) -> rule2))]
("lion" "chases" "bear" "+")
((triple1 triple3) -> (rule2 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion does not chase the bear.
False
3
inv-proof
[(((triple1 triple3) -> rule2))]
("lion" "chases" "bear" "-")
((triple1 triple3) -> (rule2 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear sees the lion.
True
5
proof
[(((triple1 ((triple1 triple3) -> rule2)) -> rule1))]
("bear" "sees" "lion" "+")
((triple1 ((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The bear does not see the lion.
False
5
inv-proof
[(((triple1 ((triple1 triple3) -> rule2)) -> rule1))]
("bear" "sees" "lion" "-")
((triple1 ((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear chases the lion.[(triple1)] The lion is young.[(triple2)] The lion sees the bear.[(triple3)] @1: The lion chases the bear.[(((triple1 triple3) -> rule2))] @2: The bear sees the lion.[(((triple1 ((triple1 triple3) -> rule2)) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The lion sees the bear.
("lion" "sees" "bear" "+")
triple3
The lion chases the bear.
("lion" "chases" "bear" "+")
((triple1 triple3) -> (rule2 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple1 ((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2