The bear is cold. The bear likes the rabbit. The bear needs the mouse. The bear needs the rabbit. The cat chases the mouse. The cat chases the rabbit. The cat needs the mouse. The mouse is nice. The mouse needs the rabbit. The rabbit chases the mouse. The rabbit is rough. The rabbit needs the bear. If the bear chases the mouse then the bear is rough. If the bear likes the rabbit then the rabbit needs the bear. If the cat likes the mouse then the mouse needs the cat. If something needs the bear then the bear chases the mouse. If the rabbit chases the mouse and the mouse is young then the rabbit chases the bear. If something is young and it needs the mouse then the mouse chases the bear. Rough things are big. If something needs the cat and the cat chases the bear then it is big.
The bear is cold.
("bear" "is" "cold" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
If the bear chases the mouse then the bear is rough.
((("bear" "chases" "mouse" "+")) -> ("bear" "is" "rough" "+"))
If the bear likes the rabbit then the rabbit needs the bear.
((("bear" "likes" "rabbit" "+")) -> ("rabbit" "needs" "bear" "+"))
If the cat likes the mouse then the mouse needs the cat.
((("cat" "likes" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If something needs the bear then the bear chases the mouse.
((("something" "needs" "bear" "+")) -> ("bear" "chases" "mouse" "+"))
If the rabbit chases the mouse and the mouse is young then the rabbit chases the bear.
((("rabbit" "chases" "mouse" "+") ("mouse" "is" "young" "+")) -> ("rabbit" "chases" "bear" "+"))
If something is young and it needs the mouse then the mouse chases the bear.
((("something" "is" "young" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "chases" "bear" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something needs the cat and the cat chases the bear then it is big.
((("something" "needs" "cat" "+") ("cat" "chases" "bear" "+")) -> ("something" "is" "big" "+"))
The bear is cold.
True
1
proof
[(triple1)]
("bear" "is" "cold" "+")
triple1
The bear does not need the mouse.
False
1
inv-proof
[(triple3)]
("bear" "needs" "mouse" "-")
triple3
The bear chases the mouse.
True
2
proof
[(((triple12) -> rule4) OR ((((triple2) -> rule2)) -> rule4))]
("bear" "chases" "mouse" "+")
((triple12) -> (rule4 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit is not big.
False
2
inv-proof
[(((triple11) -> rule7))]
("rabbit" "is" "big" "-")
((triple11) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The bear is rough.
True
3
proof
[(((((triple12) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule4)) -> rule1))]
("bear" "is" "rough" "+")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int3
The bear is not rough.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule4)) -> rule1))]
("bear" "is" "rough" "-")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int3
The bear is big.
True
4
proof
[(((((((triple12) -> rule4)) -> rule1)) -> rule7) OR ((((((((triple2) -> rule2)) -> rule4)) -> rule1)) -> rule7))]
("bear" "is" "big" "+")
((((((triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int4
The bear is not big.
False
4
inv-proof
[(((((((triple12) -> rule4)) -> rule1)) -> rule7) OR ((((((((triple2) -> rule2)) -> rule4)) -> rule1)) -> rule7))]
("bear" "is" "big" "-")
((((((triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int4
The mouse does not need the cat.
Unknown
inv-rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "cat" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "big" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "big" "-")
The rabbit chases the bear.
Unknown
rconc
[@1: The rabbit chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "bear" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The cat likes the rabbit.
Unknown
random
[@0: The cat likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "rabbit" "+")
The bear does not need the cat.
Unknown
inv-random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "-")
The mouse likes the bear.
Unknown
random
[@0: The mouse likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bear" "+")
@0: The bear is cold.[(triple1)] The bear likes the rabbit.[(triple2)] The bear needs the mouse.[(triple3)] The bear needs the rabbit.[(triple4)] The cat chases the mouse.[(triple5)] The cat chases the rabbit.[(triple6)] The cat needs the mouse.[(triple7)] The mouse is nice.[(triple8)] The mouse needs the rabbit.[(triple9)] The rabbit chases the mouse.[(triple10)] The rabbit is rough.[(triple11)] The rabbit needs the bear.[(triple12 OR ((triple2) -> rule2))] @1: The bear chases the mouse.[(((triple12) -> rule4) OR ((((triple2) -> rule2)) -> rule4))] The rabbit is big.[(((triple11) -> rule7))] @2: The bear is rough.[(((((triple12) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule4)) -> rule1))] @3: The bear is big.[(((((((triple12) -> rule4)) -> rule1)) -> rule7) OR ((((((((triple2) -> rule2)) -> rule4)) -> rule1)) -> rule7))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple4
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple5
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple6
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple12
((triple2) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((triple12) -> (rule4 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((triple11) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int3
The bear is big.
("bear" "is" "big" "+")
((((((triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int4