The bear is not nice. The bear needs the rabbit. The cow is big. The cow is kind. The mouse is big. The mouse is nice. The mouse needs the rabbit. The mouse sees the bear. The mouse sees the rabbit. The rabbit eats the bear. The rabbit eats the cow. The rabbit is big. The rabbit is cold. The rabbit is not kind. The rabbit needs the mouse. If the cow eats the rabbit then the cow needs the bear. If someone needs the bear then the bear sees the mouse. If someone sees the bear and they need the mouse then the mouse is cold. If someone sees the cow and the cow is not kind then they need the rabbit. If someone sees the mouse and they are not blue then they eat the mouse. If the bear needs the mouse and the bear is blue then the mouse sees the bear. If someone needs the mouse and the mouse eats the cow then the cow sees the mouse. If someone is kind then they eat the rabbit.
The bear is not nice.
("bear" "is" "nice" "-")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is kind.
("cow" "is" "kind" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If the cow eats the rabbit then the cow needs the bear.
((("cow" "eats" "rabbit" "+")) -> ("cow" "needs" "bear" "+"))
If someone needs the bear then the bear sees the mouse.
((("someone" "needs" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone sees the bear and they need the mouse then the mouse is cold.
((("someone" "sees" "bear" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If someone sees the cow and the cow is not kind then they need the rabbit.
((("someone" "sees" "cow" "+") ("cow" "is" "kind" "~")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the mouse and they are not blue then they eat the mouse.
((("someone" "sees" "mouse" "+") ("someone" "is" "blue" "~")) -> ("someone" "eats" "mouse" "+"))
If the bear needs the mouse and the bear is blue then the mouse sees the bear.
((("bear" "needs" "mouse" "+") ("bear" "is" "blue" "+")) -> ("mouse" "sees" "bear" "+"))
If someone needs the mouse and the mouse eats the cow then the cow sees the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "eats" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If someone is kind then they eat the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "rabbit" "+"))
The bear is not nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The bear does not need the rabbit.
False
1
inv-proof
[(triple2)]
("bear" "needs" "rabbit" "-")
triple2
The cow eats the rabbit.
True
2
proof
[(((triple4) -> rule8))]
("cow" "eats" "rabbit" "+")
((triple4) -> (rule8 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow does not eat the rabbit.
False
2
inv-proof
[(((triple4) -> rule8))]
("cow" "eats" "rabbit" "-")
((triple4) -> (rule8 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow needs the bear.
True
3
proof
[(((((triple4) -> rule8)) -> rule1))]
("cow" "needs" "bear" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow does not need the bear.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule1))]
("cow" "needs" "bear" "-")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The bear sees the mouse.
True
4
proof
[(((((((triple4) -> rule8)) -> rule1)) -> rule2))]
("bear" "sees" "mouse" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The bear does not see the mouse.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule1)) -> rule2))]
("bear" "sees" "mouse" "-")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The bear does not eat the rabbit.
Unknown
inv-rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "eats" "rabbit" "-")
The mouse eats the rabbit.
Unknown
rconc
[@1: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "rabbit" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The mouse does not eat the cow.
Unknown
inv-random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "-")
The rabbit sees the mouse.
Unknown
random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "+")
@0: The bear is not nice.[(triple1)] The bear needs the rabbit.[(triple2)] The cow is big.[(triple3)] The cow is kind.[(triple4)] The mouse is big.[(triple5)] The mouse is nice.[(triple6)] The mouse needs the rabbit.[(triple7)] The mouse sees the bear.[(triple8)] The mouse sees the rabbit.[(triple9)] The rabbit eats the bear.[(triple10)] The rabbit eats the cow.[(triple11)] The rabbit is big.[(triple12)] The rabbit is cold.[(triple13)] The rabbit is not kind.[(triple14)] The rabbit needs the mouse.[(triple15)] @1: The cow eats the rabbit.[(((triple4) -> rule8))] @2: The cow needs the bear.[(((((triple4) -> rule8)) -> rule1))] @3: The bear sees the mouse.[(((((((triple4) -> rule8)) -> rule1)) -> rule2))]
The bear is not nice.
("bear" "is" "nice" "-")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple7
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple10
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple11
The rabbit is big.
("rabbit" "is" "big" "+")
triple12
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple13
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple14
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple15
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((triple4) -> (rule8 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3