The bear chases the rabbit. The bear needs the mouse. The bear needs the rabbit. The mouse chases the bear. The mouse chases the rabbit. The rabbit is red. The rabbit likes the bear. If something is red then it chases the rabbit. If something needs the mouse then the mouse is red. If something is red then it needs the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
If something is red then it chases the rabbit.
((("something" "is" "red" "+")) -> ("something" "chases" "rabbit" "+"))
If something needs the mouse then the mouse is red.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If something is red then it needs the bear.
((("something" "is" "red" "+")) -> ("something" "needs" "bear" "+"))
The rabbit likes the bear.
True
1
proof
[(triple7)]
("rabbit" "likes" "bear" "+")
triple7
The rabbit does not like the bear.
False
1
inv-proof
[(triple7)]
("rabbit" "likes" "bear" "-")
triple7
The mouse is red.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple6) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The mouse needs the bear.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("mouse" "needs" "bear" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not need the bear.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("mouse" "needs" "bear" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
The bear does not like the mouse.
Unknown
inv-random
[@0: The bear likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "mouse" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The bear chases the rabbit.[(triple1)] The bear needs the mouse.[(triple2)] The bear needs the rabbit.[(triple3)] The mouse chases the bear.[(triple4)] The mouse chases the rabbit.[(triple5 OR ((((triple2) -> rule2)) -> rule1))] The rabbit is red.[(triple6)] The rabbit likes the bear.[(triple7)] @1: The mouse is red.[(((triple2) -> rule2))] The rabbit chases the rabbit.[(((triple6) -> rule1))] The rabbit needs the bear.[(((triple6) -> rule3))] @2: The mouse needs the bear.[(((((triple2) -> rule2)) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple6) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((triple6) -> (rule3 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2