The bald eagle is round. The dog visits the lion. The lion does not chase the mouse. The mouse visits the dog. If someone visits the dog then they like the mouse. If someone likes the mouse then the mouse likes the dog. If the bald eagle chases the mouse then the mouse is green. If the mouse does not visit the dog then the mouse does not visit the lion. If the mouse is nice and the mouse likes the dog then the mouse does not visit the lion. If someone likes the dog then they chase the mouse. If someone visits the dog then the dog likes the bald eagle. If someone visits the lion and they chase the bald eagle then the bald eagle is green.
The bald eagle is round.
("bald eagle" "is" "round" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone visits the dog then they like the mouse.
((("someone" "visits" "dog" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then the mouse likes the dog.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If the bald eagle chases the mouse then the mouse is green.
((("bald eagle" "chases" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If the mouse does not visit the dog then the mouse does not visit the lion.
((("mouse" "visits" "dog" "~")) -> ("mouse" "visits" "lion" "-"))
If the mouse is nice and the mouse likes the dog then the mouse does not visit the lion.
((("mouse" "is" "nice" "+") ("mouse" "likes" "dog" "+")) -> ("mouse" "visits" "lion" "-"))
If someone likes the dog then they chase the mouse.
((("someone" "likes" "dog" "+")) -> ("someone" "chases" "mouse" "+"))
If someone visits the dog then the dog likes the bald eagle.
((("someone" "visits" "dog" "+")) -> ("dog" "likes" "bald eagle" "+"))
If someone visits the lion and they chase the bald eagle then the bald eagle is green.
((("someone" "visits" "lion" "+") ("someone" "chases" "bald eagle" "+")) -> ("bald eagle" "is" "green" "+"))
The lion does not chase the mouse.
True
1
proof
[(triple3)]
("lion" "chases" "mouse" "-")
triple3
The lion chases the mouse.
False
1
inv-proof
[(triple3)]
("lion" "chases" "mouse" "+")
triple3
The mouse likes the mouse.
True
2
proof
[(((triple4) -> rule1))]
("mouse" "likes" "mouse" "+")
((triple4) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The dog does not like the bald eagle.
False
2
inv-proof
[(((triple4) -> rule7))]
("dog" "likes" "bald eagle" "-")
((triple4) -> (rule7 % int1))
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
int1
The mouse likes the dog.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("mouse" "likes" "dog" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse does not like the dog.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("mouse" "likes" "dog" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule6))]
("mouse" "chases" "mouse" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule6))]
("mouse" "chases" "mouse" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The lion does not like the mouse.
Unknown
inv-rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "mouse" "-")
The mouse is green.
Unknown
rconc
[@2: The mouse is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("mouse" "is" "green" "+")
The bald eagle does not like the mouse.
Unknown
inv-rconc
[@1: The bald eagle likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "likes" "mouse" "-")
The dog chases the mouse.
Unknown
rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "mouse" "+")
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 dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The lion visits the mouse.
Unknown
random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "+")
@0: The bald eagle is round.[(triple1)] The dog visits the lion.[(triple2)] The lion does not chase the mouse.[(triple3)] The mouse visits the dog.[(triple4)] @1: The dog likes the bald eagle.[(((triple4) -> rule7))] The mouse likes the mouse.[(((triple4) -> rule1))] @2: The mouse likes the dog.[(((((triple4) -> rule1)) -> rule2))] @3: The mouse chases the mouse.[(((((((triple4) -> rule1)) -> rule2)) -> rule6))]
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple2
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
triple3
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple4
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
((triple4) -> (rule7 % int1))
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple4) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3