The bear needs the mouse. The cat is nice. The cat needs the rabbit. The mouse is nice. The mouse sees the cat. The rabbit eats the bear. The rabbit needs the mouse. If someone needs the rabbit then they need the mouse. Cold people are nice. If someone needs the rabbit then they need the cat. If someone sees the rabbit and they are cold then the rabbit is rough. If the cat eats the rabbit and the rabbit eats the mouse then the mouse needs the rabbit. If someone is red then they need the bear. If someone eats the mouse and they are blue then the mouse is red. If someone needs the mouse then they are red.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If someone needs the rabbit then they need the mouse.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "mouse" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the rabbit then they need the cat.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "cat" "+"))
If someone sees the rabbit and they are cold then the rabbit is rough.
((("someone" "sees" "rabbit" "+") ("someone" "is" "cold" "+")) -> ("rabbit" "is" "rough" "+"))
If the cat eats the rabbit and the rabbit eats the mouse then the mouse needs the rabbit.
((("cat" "eats" "rabbit" "+") ("rabbit" "eats" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone is red then they need the bear.
((("someone" "is" "red" "+")) -> ("someone" "needs" "bear" "+"))
If someone eats the mouse and they are blue then the mouse is red.
((("someone" "eats" "mouse" "+") ("someone" "is" "blue" "+")) -> ("mouse" "is" "red" "+"))
If someone needs the mouse then they are red.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "red" "+"))
The rabbit needs the mouse.
True
1
proof
[(triple7)]
("rabbit" "needs" "mouse" "+")
triple7
The bear does not need the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "-")
triple1
The cat needs the mouse.
True
2
proof
[(((triple3) -> rule1))]
("cat" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "needs" "mouse" "-")
((triple3) -> (rule1 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The bear needs the bear.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("bear" "needs" "bear" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear does not need the bear.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6))]
("bear" "needs" "bear" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The cat needs the bear.
True
4
proof
[(((((((triple3) -> rule1)) -> rule8)) -> rule6))]
("cat" "needs" "bear" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The cat does not need the bear.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule8)) -> rule6))]
("cat" "needs" "bear" "-")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "nice" "-")
The mouse needs the rabbit.
Unknown
rconc
[@1: The mouse needs the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "rabbit" "+")
The rabbit does not need the cat.
Unknown
inv-rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "cat" "-")
The mouse needs the bear.
Unknown
rconc
[@4: The mouse needs the bear.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule1 <- rule5 <- FAIL)]]
("mouse" "needs" "bear" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The bear eats the cat.
Unknown
random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse sees the rabbit.
Unknown
random
[@0: The mouse sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "rabbit" "+")
@0: The bear needs the mouse.[(triple1)] The cat is nice.[(triple2)] The cat needs the rabbit.[(triple3)] The mouse is nice.[(triple4)] The mouse sees the cat.[(triple5)] The rabbit eats the bear.[(triple6)] The rabbit needs the mouse.[(triple7)] @1: The bear is red.[(((triple1) -> rule8))] The cat needs the cat.[(((triple3) -> rule3))] The cat needs the mouse.[(((triple3) -> rule1))] The rabbit is red.[(((triple7) -> rule8))] @2: The bear needs the bear.[(((((triple1) -> rule8)) -> rule6))] The cat is red.[(((((triple3) -> rule1)) -> rule8))] The rabbit needs the bear.[(((((triple7) -> rule8)) -> rule6))] @3: The cat needs the bear.[(((((((triple3) -> rule1)) -> rule8)) -> rule6))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple5
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple6
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple7
The bear is red.
("bear" "is" "red" "+")
((triple1) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple3) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple7) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((((triple7) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3