The bear chases the rabbit. The bear is young. The bear needs the cow. The cow is kind. The cow is red. The cow is young. The rabbit is young. If something chases the rabbit then it likes the cow. If something is young and rough then it chases the bear. If something likes the bear and it likes the cow then the cow does not need the bear. Young things are rough. If something likes the cow then it needs the rabbit. If something is rough then it likes the bear. If something chases the rabbit then it is kind. If something likes the bear and it does not like the cow then the bear likes the rabbit.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If something chases the rabbit then it likes the cow.
((("something" "chases" "rabbit" "+")) -> ("something" "likes" "cow" "+"))
If something is young and rough then it chases the bear.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "chases" "bear" "+"))
If something likes the bear and it likes the cow then the cow does not need the bear.
((("something" "likes" "bear" "+") ("something" "likes" "cow" "+")) -> ("cow" "needs" "bear" "-"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something likes the cow then it needs the rabbit.
((("something" "likes" "cow" "+")) -> ("something" "needs" "rabbit" "+"))
If something is rough then it likes the bear.
((("something" "is" "rough" "+")) -> ("something" "likes" "bear" "+"))
If something chases the rabbit then it is kind.
((("something" "chases" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If something likes the bear and it does not like the cow then the bear likes the rabbit.
((("something" "likes" "bear" "+") ("something" "likes" "cow" "~")) -> ("bear" "likes" "rabbit" "+"))
The cow is kind.
True
1
proof
[(triple4)]
("cow" "is" "kind" "+")
triple4
The cow is not kind.
False
1
inv-proof
[(triple4)]
("cow" "is" "kind" "-")
triple4
The bear is kind.
True
2
proof
[(((triple1) -> rule7))]
("bear" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear does not like the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "likes" "cow" "-")
((triple1) -> (rule1 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The cow likes the bear.
True
3
proof
[(((((triple6) -> rule4)) -> rule6))]
("cow" "likes" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The bear does not like the bear.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("bear" "likes" "bear" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The cow does not need the bear.
True
6
proof
[(((((((triple2) -> rule4)) -> rule6) ((triple1) -> rule1)) -> rule3))]
("cow" "needs" "bear" "-")
((((((triple2) -> (rule4 % int4))) -> (rule6 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow does not need the bear.
("cow" "needs" "bear" "-")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
int4
The cow needs the bear.
False
6
inv-proof
[(((((((triple2) -> rule4)) -> rule6) ((triple1) -> rule1)) -> rule3))]
("cow" "needs" "bear" "+")
((((((triple2) -> (rule4 % int4))) -> (rule6 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow does not need the bear.
("cow" "needs" "bear" "-")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
int4
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "-")
The rabbit likes the cow.
Unknown
rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "cow" "+")
The bear does not like the rabbit.
Unknown
inv-rconc
[@1: The bear likes the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "likes" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit does not chase the cow.
Unknown
inv-random
[@0: The rabbit chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cow" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
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 cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is young.[(triple2)] The bear needs the cow.[(triple3)] The cow is kind.[(triple4)] The cow is red.[(triple5)] The cow is young.[(triple6)] The rabbit is young.[(triple7)] @1: The bear is kind.[(((triple1) -> rule7))] The bear is rough.[(((triple2) -> rule4))] The bear likes the cow.[(((triple1) -> rule1))] The cow is rough.[(((triple6) -> rule4))] The rabbit is rough.[(((triple7) -> rule4))] @2: The bear chases the bear.[(((triple2 ((triple2) -> rule4)) -> rule2))] The bear likes the bear.[(((((triple2) -> rule4)) -> rule6))] The bear needs the rabbit.[(((((triple1) -> rule1)) -> rule5))] The cow chases the bear.[(((triple6 ((triple6) -> rule4)) -> rule2))] The cow likes the bear.[(((((triple6) -> rule4)) -> rule6))] The rabbit chases the bear.[(((triple7 ((triple7) -> rule4)) -> rule2))] The rabbit likes the bear.[(((((triple7) -> rule4)) -> rule6))] @3: The cow does not need the bear.[(((((((triple2) -> rule4)) -> rule6) ((triple1) -> rule1)) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The bear is kind.
("bear" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple6) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple7) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow does not need the bear.
("cow" "needs" "bear" "-")
((((((triple2) -> (rule4 % int4))) -> (rule6 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow does not need the bear.
("cow" "needs" "bear" "-")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
int4