The bald eagle sees the cat. The cat likes the mouse. The mouse sees the bald eagle. The squirrel sees the mouse. If something is round and it likes the mouse then it is red. If something sees the mouse then the mouse is rough. If the cat is nice then the cat does not like the squirrel. If the bald eagle chases the squirrel then the bald eagle likes the squirrel. If something chases the bald eagle then the bald eagle is not rough. If something is rough then it chases the bald eagle.
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something is round and it likes the mouse then it is red.
((("something" "is" "round" "+") ("something" "likes" "mouse" "+")) -> ("something" "is" "red" "+"))
If something sees the mouse then the mouse is rough.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If the cat is nice then the cat does not like the squirrel.
((("cat" "is" "nice" "+")) -> ("cat" "likes" "squirrel" "-"))
If the bald eagle chases the squirrel then the bald eagle likes the squirrel.
((("bald eagle" "chases" "squirrel" "+")) -> ("bald eagle" "likes" "squirrel" "+"))
If something chases the bald eagle then the bald eagle is not rough.
((("something" "chases" "bald eagle" "+")) -> ("bald eagle" "is" "rough" "-"))
If something is rough then it chases the bald eagle.
((("something" "is" "rough" "+")) -> ("something" "chases" "bald eagle" "+"))
The mouse sees the bald eagle.
True
1
proof
[(triple3)]
("mouse" "sees" "bald eagle" "+")
triple3
The cat does not like the mouse.
False
1
inv-proof
[(triple2)]
("cat" "likes" "mouse" "-")
triple2
The mouse is rough.
True
2
proof
[(((triple4) -> rule2))]
("mouse" "is" "rough" "+")
((triple4) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple4) -> rule2))]
("mouse" "is" "rough" "-")
((triple4) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the bald eagle.
True
3
proof
[(((((triple4) -> rule2)) -> rule6))]
("mouse" "chases" "bald eagle" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not chase the bald eagle.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule6))]
("mouse" "chases" "bald eagle" "-")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bald eagle is not rough.
True
4
proof
[(((((((triple4) -> rule2)) -> rule6)) -> rule5))]
("bald eagle" "is" "rough" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle is not rough.
("bald eagle" "is" "rough" "-")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The bald eagle is rough.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule6)) -> rule5))]
("bald eagle" "is" "rough" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle is not rough.
("bald eagle" "is" "rough" "-")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "red" "-")
The bald eagle is red.
Unknown
rconc
[@1: The bald eagle is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "red" "+")
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "red" "-")
The squirrel is red.
Unknown
rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "red" "+")
The squirrel does not like the mouse.
Unknown
inv-random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat does not chase the mouse.
Unknown
inv-random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "-")
The cat sees the bald eagle.
Unknown
random
[@0: The cat sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bald eagle" "+")
@0: The bald eagle sees the cat.[(triple1)] The cat likes the mouse.[(triple2)] The mouse sees the bald eagle.[(triple3)] The squirrel sees the mouse.[(triple4)] @1: The mouse is rough.[(((triple4) -> rule2))] @2: The mouse chases the bald eagle.[(((((triple4) -> rule2)) -> rule6))] @3: The bald eagle is not rough.[(((((((triple4) -> rule2)) -> rule6)) -> rule5))]
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple2
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
triple3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
((triple4) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bald eagle is not rough.
("bald eagle" "is" "rough" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle is not rough.
("bald eagle" "is" "rough" "-")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3