The bald eagle needs the dog. The dog is red. The mouse chases the dog. If the bald eagle needs the mouse then the mouse visits the dog. All red people are not big. If someone visits the mouse and the mouse is big then the mouse is blue. If someone chases the dog then they visit the dog. If someone is nice then they chase the mouse. If someone visits the bald eagle then they need the dog. If someone visits the dog then they need the dog. If the bald eagle chases the dog then the dog needs the bald eagle.
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
If the bald eagle needs the mouse then the mouse visits the dog.
((("bald eagle" "needs" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
All red people are not big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "-"))
If someone visits the mouse and the mouse is big then the mouse is blue.
((("someone" "visits" "mouse" "+") ("mouse" "is" "big" "+")) -> ("mouse" "is" "blue" "+"))
If someone chases the dog then they visit the dog.
((("someone" "chases" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone is nice then they chase the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "mouse" "+"))
If someone visits the bald eagle then they need the dog.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "needs" "dog" "+"))
If someone visits the dog then they need the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If the bald eagle chases the dog then the dog needs the bald eagle.
((("bald eagle" "chases" "dog" "+")) -> ("dog" "needs" "bald eagle" "+"))
The mouse chases the dog.
True
1
proof
[(triple3)]
("mouse" "chases" "dog" "+")
triple3
The dog is not red.
False
1
inv-proof
[(triple2)]
("dog" "is" "red" "-")
triple2
The mouse visits the dog.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog is big.
False
2
inv-proof
[(((triple2) -> rule2))]
("dog" "is" "big" "+")
((triple2) -> (rule2 % int1))
The dog is not big.
("dog" "is" "big" "-")
int1
The mouse needs the dog.
True
3
proof
[(((((triple3) -> rule4)) -> rule7))]
("mouse" "needs" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The mouse does not need the dog.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule7))]
("mouse" "needs" "dog" "-")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The dog does not need the dog.
Unknown
inv-rconc
[@2: The dog needs the dog.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog chases the mouse.
Unknown
rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The bald eagle is nice.
Unknown
random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "+")
The mouse does not need the bald eagle.
Unknown
inv-random
[@0: The mouse needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bald eagle" "-")
The dog needs the mouse.
Unknown
random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "+")
@0: The bald eagle needs the dog.[(triple1)] The dog is red.[(triple2)] The mouse chases the dog.[(triple3)] @1: The dog is not big.[(((triple2) -> rule2))] The mouse visits the dog.[(((triple3) -> rule4))] @2: The mouse needs the dog.[(((((triple3) -> rule4)) -> rule7))]
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The dog is not big.
("dog" "is" "big" "-")
((triple2) -> (rule2 % int1))
The dog is not big.
("dog" "is" "big" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2