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