The bald eagle chases the dog. The bald eagle is blue. The bald eagle is green. The bald eagle is round. The bald eagle needs the dog. The dog needs the bald eagle. The dog needs the mouse. The dog visits the mouse. The mouse chases the bald eagle. The mouse chases the dog. The mouse is green. The mouse is nice. The mouse is round. The mouse needs the bald eagle. The mouse visits the dog. If something needs the mouse and the mouse is nice then it chases the dog. If something visits the bald eagle then it is round. If the mouse chases the dog then the dog visits the mouse. If something needs the mouse and it is nice then the mouse needs the dog. If the dog chases the bald eagle and the bald eagle needs the dog then the dog visits the mouse. If something needs the bald eagle and it visits the mouse then the mouse is nice.
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something needs the mouse and the mouse is nice then it chases the dog.
((("something" "needs" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("something" "chases" "dog" "+"))
If something visits the bald eagle then it is round.
((("something" "visits" "bald eagle" "+")) -> ("something" "is" "round" "+"))
If the mouse chases the dog then the dog visits the mouse.
((("mouse" "chases" "dog" "+")) -> ("dog" "visits" "mouse" "+"))
If something needs the mouse and it is nice then the mouse needs the dog.
((("something" "needs" "mouse" "+") ("something" "is" "nice" "+")) -> ("mouse" "needs" "dog" "+"))
If the dog chases the bald eagle and the bald eagle needs the dog then the dog visits the mouse.
((("dog" "chases" "bald eagle" "+") ("bald eagle" "needs" "dog" "+")) -> ("dog" "visits" "mouse" "+"))
If something needs the bald eagle and it visits the mouse then the mouse is nice.
((("something" "needs" "bald eagle" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
The mouse needs the bald eagle.
True
1
proof
[(triple14)]
("mouse" "needs" "bald eagle" "+")
triple14
The mouse does not chase the dog.
False
1
inv-proof
[(triple10)]
("mouse" "chases" "dog" "-")
triple10
The dog chases the dog.
True
3
proof
[(((triple7 triple12) -> rule1) OR ((triple7 ((triple6 triple8) -> rule6)) -> rule1) OR ((triple7 ((triple6 ((triple10) -> rule3)) -> rule6)) -> rule1))]
("dog" "chases" "dog" "+")
((triple7 triple12) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
((triple7 ((triple6 triple8) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((triple7 ((triple6 ((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The dog does not chase the dog.
False
3
inv-proof
[(((triple7 triple12) -> rule1) OR ((triple7 ((triple6 triple8) -> rule6)) -> rule1) OR ((triple7 ((triple6 ((triple10) -> rule3)) -> rule6)) -> rule1))]
("dog" "chases" "dog" "-")
((triple7 triple12) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
((triple7 ((triple6 triple8) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((triple7 ((triple6 ((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "round" "-")
The mouse needs the dog.
Unknown
rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "dog" "+")
The mouse does not visit the bald eagle.
Unknown
inv-random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The bald eagle chases the dog.[(triple1)] The bald eagle is blue.[(triple2)] The bald eagle is green.[(triple3)] The bald eagle is round.[(triple4)] The bald eagle needs the dog.[(triple5)] The dog needs the bald eagle.[(triple6)] The dog needs the mouse.[(triple7)] The dog visits the mouse.[(triple8 OR ((triple10) -> rule3))] The mouse chases the bald eagle.[(triple9)] The mouse chases the dog.[(triple10)] The mouse is green.[(triple11)] The mouse is nice.[(triple12 OR ((triple6 triple8) -> rule6) OR ((triple6 ((triple10) -> rule3)) -> rule6))] The mouse is round.[(triple13)] The mouse needs the bald eagle.[(triple14)] The mouse visits the dog.[(triple15)] @1: The dog chases the dog.[(((triple7 triple12) -> rule1) OR ((triple7 ((triple6 triple8) -> rule6)) -> rule1) OR ((triple7 ((triple6 ((triple10) -> rule3)) -> rule6)) -> rule1))]
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
triple1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple2
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple3
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple4
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple5
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple6
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple8
((triple10) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple9
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
((triple6 triple8) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((triple6 ((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple14
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple15
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple7 triple12) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
((triple7 ((triple6 triple8) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((triple7 ((triple6 ((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3