The bald eagle needs the mouse. The cat needs the mouse. The cow is big. The mouse likes the bald eagle. If something is red and it likes the cow then it needs the mouse. If something sees the cat then it needs the cow. If something needs the mouse and the mouse is red then the mouse sees the cow. If something is nice then it likes the cow. If something needs the mouse then the mouse is red. All young things are kind.
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
If something is red and it likes the cow then it needs the mouse.
((("something" "is" "red" "+") ("something" "likes" "cow" "+")) -> ("something" "needs" "mouse" "+"))
If something sees the cat then it needs the cow.
((("something" "sees" "cat" "+")) -> ("something" "needs" "cow" "+"))
If something needs the mouse and the mouse is red then the mouse sees the cow.
((("something" "needs" "mouse" "+") ("mouse" "is" "red" "+")) -> ("mouse" "sees" "cow" "+"))
If something is nice then it likes the cow.
((("something" "is" "nice" "+")) -> ("something" "likes" "cow" "+"))
If something needs the mouse then the mouse is red.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "red" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
The cat needs the mouse.
True
1
proof
[(triple2)]
("cat" "needs" "mouse" "+")
triple2
The bald eagle does not need the mouse.
False
1
inv-proof
[(triple1)]
("bald eagle" "needs" "mouse" "-")
triple1
The mouse is red.
True
2
proof
[(((triple1) -> rule5) OR ((triple2) -> rule5))]
("mouse" "is" "red" "+")
((triple1) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((triple2) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple2) -> rule5))]
("mouse" "is" "red" "-")
((triple1) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((triple2) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the cow.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule3) OR ((triple1 ((triple2) -> rule5)) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))]
("mouse" "sees" "cow" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple1 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not see the cow.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule3) OR ((triple1 ((triple2) -> rule5)) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))]
("mouse" "sees" "cow" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple1 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The bald eagle is not kind.
Unknown
inv-rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The cat likes the cow.
Unknown
rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "cow" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse sees the bald eagle.
Unknown
random
[@0: The mouse sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bald eagle" "+")
The cow does not see the bald eagle.
Unknown
inv-random
[@0: The cow sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bald eagle" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The bald eagle needs the mouse.[(triple1)] The cat needs the mouse.[(triple2)] The cow is big.[(triple3)] The mouse likes the bald eagle.[(triple4)] @1: The mouse is red.[(((triple1) -> rule5) OR ((triple2) -> rule5))] @2: The mouse sees the cow.[(((triple1 ((triple1) -> rule5)) -> rule3) OR ((triple1 ((triple2) -> rule5)) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))]
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
((triple1) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((triple2) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple1 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2