The bear is green. The cow likes the mouse. The cow needs the mouse. The mouse eats the cow. The mouse is rough. The mouse likes the bear. The rabbit eats the cow. If something needs the mouse then the mouse is round. If something is round then it needs the mouse. If something is rough and it needs the mouse then the mouse needs the bear.
The bear is green.
("bear" "is" "green" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
If something needs the mouse then the mouse is round.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something is round then it needs the mouse.
((("something" "is" "round" "+")) -> ("something" "needs" "mouse" "+"))
If something is rough and it needs the mouse then the mouse needs the bear.
((("something" "is" "rough" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
The rabbit eats the cow.
True
1
proof
[(triple7)]
("rabbit" "eats" "cow" "+")
triple7
The cow does not like the mouse.
False
1
inv-proof
[(triple2)]
("cow" "likes" "mouse" "-")
triple2
The mouse is round.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "is" "round" "+")
((triple3) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "is" "round" "-")
((triple3) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("mouse" "needs" "mouse" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the bear.
True
5
proof
[(((triple5 ((((triple3) -> rule1)) -> rule2)) -> rule3))]
("mouse" "needs" "bear" "+")
((triple5 ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The mouse does not need the bear.
False
5
inv-proof
[(((triple5 ((((triple3) -> rule1)) -> rule2)) -> rule3))]
("mouse" "needs" "bear" "-")
((triple5 ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The bear does not need the mouse.
Unknown
inv-rconc
[@1: The bear needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "mouse" "-")
The rabbit needs the mouse.
Unknown
rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "mouse" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The bear does not eat the mouse.
Unknown
inv-random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The bear is green.[(triple1)] The cow likes the mouse.[(triple2)] The cow needs the mouse.[(triple3)] The mouse eats the cow.[(triple4)] The mouse is rough.[(triple5)] The mouse likes the bear.[(triple6)] The rabbit eats the cow.[(triple7)] @1: The mouse is round.[(((triple3) -> rule1))] @2: The mouse needs the mouse.[(((((triple3) -> rule1)) -> rule2))] @3: The mouse needs the bear.[(((triple5 ((((triple3) -> rule1)) -> rule2)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple6
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple7
The mouse is round.
("mouse" "is" "round" "+")
((triple3) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple5 ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3