The bear is nice. The cow likes the rabbit. The rabbit is kind. If the cow likes the rabbit and the cow is nice then the rabbit needs the bear. If something likes the rabbit then the rabbit needs the bear. If something is rough then it likes the cow. If the rabbit needs the bear then the rabbit is green. If something is green then it does not see the rabbit. If something likes the bear then the bear does not like the rabbit. If something is green and it does not see the rabbit then it sees the bear. If something sees the bear then it needs the rabbit.
The bear is nice.
("bear" "is" "nice" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If the cow likes the rabbit and the cow is nice then the rabbit needs the bear.
((("cow" "likes" "rabbit" "+") ("cow" "is" "nice" "+")) -> ("rabbit" "needs" "bear" "+"))
If something likes the rabbit then the rabbit needs the bear.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "needs" "bear" "+"))
If something is rough then it likes the cow.
((("something" "is" "rough" "+")) -> ("something" "likes" "cow" "+"))
If the rabbit needs the bear then the rabbit is green.
((("rabbit" "needs" "bear" "+")) -> ("rabbit" "is" "green" "+"))
If something is green then it does not see the rabbit.
((("something" "is" "green" "+")) -> ("something" "sees" "rabbit" "-"))
If something likes the bear then the bear does not like the rabbit.
((("something" "likes" "bear" "+")) -> ("bear" "likes" "rabbit" "-"))
If something is green and it does not see the rabbit then it sees the bear.
((("something" "is" "green" "+") ("something" "sees" "rabbit" "~")) -> ("something" "sees" "bear" "+"))
If something sees the bear then it needs the rabbit.
((("something" "sees" "bear" "+")) -> ("something" "needs" "rabbit" "+"))
The rabbit is kind.
True
1
proof
[(triple3)]
("rabbit" "is" "kind" "+")
triple3
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The rabbit needs the bear.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "needs" "bear" "+")
((triple2) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit does not need the bear.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "needs" "bear" "-")
((triple2) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit is green.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("rabbit" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit is not green.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("rabbit" "is" "green" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit does not see the rabbit.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
("rabbit" "sees" "rabbit" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int3
The rabbit sees the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
("rabbit" "sees" "rabbit" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int3
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cow" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "sees" "bear" "+")
The bear does not need the rabbit.
Unknown
inv-rconc
[@2: The bear needs the rabbit.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("bear" "needs" "rabbit" "-")
The cow needs the rabbit.
Unknown
rconc
[@2: The cow needs the rabbit.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("cow" "needs" "rabbit" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The bear is nice.[(triple1)] The cow likes the rabbit.[(triple2)] The rabbit is kind.[(triple3)] @1: The rabbit needs the bear.[(((triple2) -> rule2))] @2: The rabbit is green.[(((((triple2) -> rule2)) -> rule4))] @3: The rabbit does not see the rabbit.[(((((((triple2) -> rule2)) -> rule4)) -> rule5))] @4: The rabbit sees the bear.[(((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule2)) -> rule4)) -> rule5)) -> rule7))] @5: The rabbit needs the rabbit.[(((((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule2)) -> rule4)) -> rule5)) -> rule7)) -> rule8))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((triple2) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int3
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int4
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) ((((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int5