The bald eagle chases the lion. The bald eagle needs the dog. The bald eagle needs the lion. The bald eagle sees the lion. The dog chases the bald eagle. The dog is round. The dog needs the lion. The lion chases the dog. The lion chases the mouse. The lion needs the dog. The lion needs the mouse. The lion sees the dog. The mouse chases the lion. The mouse is not big. The mouse sees the dog. If something chases the lion then it sees the lion. If something is rough and it chases the dog then it chases the mouse. If something sees the lion then it sees the mouse.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something chases the lion then it sees the lion.
((("something" "chases" "lion" "+")) -> ("something" "sees" "lion" "+"))
If something is rough and it chases the dog then it chases the mouse.
((("something" "is" "rough" "+") ("something" "chases" "dog" "+")) -> ("something" "chases" "mouse" "+"))
If something sees the lion then it sees the mouse.
((("something" "sees" "lion" "+")) -> ("something" "sees" "mouse" "+"))
The lion chases the mouse.
True
1
proof
[(triple9)]
("lion" "chases" "mouse" "+")
triple9
The dog does not chase the bald eagle.
False
1
inv-proof
[(triple5)]
("dog" "chases" "bald eagle" "-")
triple5
The mouse sees the lion.
True
2
proof
[(((triple13) -> rule1))]
("mouse" "sees" "lion" "+")
((triple13) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse does not see the lion.
False
2
inv-proof
[(((triple13) -> rule1))]
("mouse" "sees" "lion" "-")
((triple13) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the mouse.
True
3
proof
[(((((triple13) -> rule1)) -> rule3))]
("mouse" "sees" "mouse" "+")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The mouse does not see the mouse.
False
3
inv-proof
[(((((triple13) -> rule1)) -> rule3))]
("mouse" "sees" "mouse" "-")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The dog chases the mouse.
Unknown
rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "mouse" "+")
The dog does not see the mouse.
Unknown
inv-rconc
[@2: The dog sees the mouse.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("dog" "sees" "mouse" "-")
The bald eagle sees the dog.
Unknown
random
[@0: The bald eagle sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "dog" "+")
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 is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The bald eagle chases the lion.[(triple1)] The bald eagle needs the dog.[(triple2)] The bald eagle needs the lion.[(triple3)] The bald eagle sees the lion.[(triple4 OR ((triple1) -> rule1))] The dog chases the bald eagle.[(triple5)] The dog is round.[(triple6)] The dog needs the lion.[(triple7)] The lion chases the dog.[(triple8)] The lion chases the mouse.[(triple9)] The lion needs the dog.[(triple10)] The lion needs the mouse.[(triple11)] The lion sees the dog.[(triple12)] The mouse chases the lion.[(triple13)] The mouse is not big.[(triple14)] The mouse sees the dog.[(triple15)] @1: The bald eagle sees the mouse.[(((triple4) -> rule3) OR ((((triple1) -> rule1)) -> rule3))] The mouse sees the lion.[(((triple13) -> rule1))] @2: The mouse sees the mouse.[(((((triple13) -> rule1)) -> rule3))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple4
((triple1) -> (rule1 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The dog needs the lion.
("dog" "needs" "lion" "+")
triple7
The lion chases the dog.
("lion" "chases" "dog" "+")
triple8
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple9
The lion needs the dog.
("lion" "needs" "dog" "+")
triple10
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple11
The lion sees the dog.
("lion" "sees" "dog" "+")
triple12
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple13
The mouse is not big.
("mouse" "is" "big" "-")
triple14
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple15
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
((triple4) -> (rule3 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple13) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2