The bald eagle is rough. The bald eagle does not see the cat. The cat needs the dog. The dog chases the cat. The dog chases the mouse. The dog is rough. The dog needs the bald eagle. The dog needs the cat. The dog needs the mouse. The dog sees the mouse. The mouse does not chase the cat. The mouse is nice. If something sees the dog then the dog needs the mouse. If something sees the mouse and the mouse sees the bald eagle then the bald eagle is rough. If something is blue and it does not need the dog then the dog sees the mouse. If something chases the mouse then it sees the mouse. If something is nice then it is not big. If something needs the mouse and the mouse is not big then it sees the cat.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle does not see the cat.
("bald eagle" "sees" "cat" "-")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
If something sees the dog then the dog needs the mouse.
((("something" "sees" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If something sees the mouse and the mouse sees the bald eagle then the bald eagle is rough.
((("something" "sees" "mouse" "+") ("mouse" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "rough" "+"))
If something is blue and it does not need the dog then the dog sees the mouse.
((("something" "is" "blue" "+") ("something" "needs" "dog" "~")) -> ("dog" "sees" "mouse" "+"))
If something chases the mouse then it sees the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something is nice then it is not big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "-"))
If something needs the mouse and the mouse is not big then it sees the cat.
((("something" "needs" "mouse" "+") ("mouse" "is" "big" "~")) -> ("something" "sees" "cat" "+"))
The dog needs the cat.
True
1
proof
[(triple8)]
("dog" "needs" "cat" "+")
triple8
The dog does not see the mouse.
False
1
inv-proof
[(triple10 OR ((triple5) -> rule4))]
("dog" "sees" "mouse" "-")
triple10
((triple5) -> (rule4 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse is not big.
True
2
proof
[(((triple12) -> rule5))]
("mouse" "is" "big" "-")
((triple12) -> (rule5 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The mouse is big.
False
2
inv-proof
[(((triple12) -> rule5))]
("mouse" "is" "big" "+")
((triple12) -> (rule5 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The dog sees the cat.
True
4
proof
[(((triple9 ((triple12) -> rule5)) -> rule6))]
("dog" "sees" "cat" "+")
((triple9 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The mouse is not big.
("mouse" "is" "big" "-")
int2
The dog does not see the cat.
False
4
inv-proof
[(((triple9 ((triple12) -> rule5)) -> rule6))]
("dog" "sees" "cat" "-")
((triple9 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The mouse is not big.
("mouse" "is" "big" "-")
int2
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "+")
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "cat" "-")
The mouse needs the bald eagle.
Unknown
random
[@0: The mouse needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bald eagle" "+")
The cat does not chase the bald eagle.
Unknown
inv-random
[@0: The cat chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bald eagle" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The bald eagle does not see the cat.[(triple2)] The bald eagle is rough.[(triple1)] The cat needs the dog.[(triple3)] The dog chases the cat.[(triple4)] The dog chases the mouse.[(triple5)] The dog is rough.[(triple6)] The dog needs the bald eagle.[(triple7)] The dog needs the cat.[(triple8)] The dog needs the mouse.[(triple9)] The dog sees the mouse.[(triple10 OR ((triple5) -> rule4))] The mouse does not chase the cat.[(triple11)] The mouse is nice.[(triple12)] @1: The mouse is not big.[(((triple12) -> rule5))] @2: The dog sees the cat.[(((triple9 ((triple12) -> rule5)) -> rule6))]
The bald eagle does not see the cat.
("bald eagle" "sees" "cat" "-")
triple2
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The dog chases the cat.
("dog" "chases" "cat" "+")
triple4
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple8
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple9
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple10
((triple5) -> (rule4 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is not big.
("mouse" "is" "big" "-")
((triple12) -> (rule5 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
((triple9 ((triple12) -> (rule5 % int2))) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The mouse is not big.
("mouse" "is" "big" "-")
int2