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