The bear is green. The dog is green. The dog is rough. The dog likes the mouse. The dog likes the rabbit. The dog visits the bear. The mouse is not blue. The mouse does not visit the dog. The rabbit is nice. The rabbit likes the dog. The rabbit likes the mouse. The rabbit visits the mouse. If something visits the rabbit then it is nice. If something is green and it visits the mouse then it is not nice. If something is round then it needs the dog. If something likes the mouse then the mouse visits the rabbit. If something is nice then it needs the bear. If something visits the mouse then it is round. If something needs the rabbit then the rabbit does not like the bear. If something needs the dog and the dog likes the rabbit then the dog visits the mouse.
The bear is green.
("bear" "is" "green" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something visits the rabbit then it is nice.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something is green and it visits the mouse then it is not nice.
((("something" "is" "green" "+") ("something" "visits" "mouse" "+")) -> ("something" "is" "nice" "-"))
If something is round then it needs the dog.
((("something" "is" "round" "+")) -> ("something" "needs" "dog" "+"))
If something likes the mouse then the mouse visits the rabbit.
((("something" "likes" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If something is nice then it needs the bear.
((("something" "is" "nice" "+")) -> ("something" "needs" "bear" "+"))
If something visits the mouse then it is round.
((("something" "visits" "mouse" "+")) -> ("something" "is" "round" "+"))
If something needs the rabbit then the rabbit does not like the bear.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "likes" "bear" "-"))
If something needs the dog and the dog likes the rabbit then the dog visits the mouse.
((("something" "needs" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("dog" "visits" "mouse" "+"))
The mouse does not visit the dog.
True
1
proof
[(triple8)]
("mouse" "visits" "dog" "-")
triple8
The rabbit is not nice.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "nice" "-")
triple9
The rabbit needs the bear.
True
2
proof
[(((triple9) -> rule5))]
("rabbit" "needs" "bear" "+")
((triple9) -> (rule5 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple12) -> rule6))]
("rabbit" "is" "round" "-")
((triple12) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The mouse is nice.
True
3
proof
[(((((triple11) -> rule4)) -> rule1) OR ((((triple4) -> rule4)) -> rule1))]
("mouse" "is" "nice" "+")
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The rabbit does not need the dog.
False
3
inv-proof
[(((((triple12) -> rule6)) -> rule3))]
("rabbit" "needs" "dog" "-")
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The mouse needs the bear.
True
4
proof
[(((((((triple11) -> rule4)) -> rule1)) -> rule5) OR ((((((triple4) -> rule4)) -> rule1)) -> rule5))]
("mouse" "needs" "bear" "+")
((((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
The dog does not visit the mouse.
False
5
inv-proof
[(((((((triple12) -> rule6)) -> rule3) triple5) -> rule8))]
("dog" "visits" "mouse" "-")
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The dog is not nice.
True
7
proof
[(((triple2 ((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule2))]
("dog" "is" "nice" "-")
((triple2 ((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The dog is not round.
False
6
inv-proof
[(((((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule6))]
("dog" "is" "round" "-")
((((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The dog needs the dog.
True
7
proof
[(((((((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule6)) -> rule3))]
("dog" "needs" "dog" "+")
((((((((((triple12) -> (rule6 % int5))) -> (rule3 % int4)) triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
int5
The dog does not need the dog.
False
7
inv-proof
[(((((((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule6)) -> rule3))]
("dog" "needs" "dog" "-")
((((((((((triple12) -> (rule6 % int5))) -> (rule3 % int4)) triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
int5
The dog does not need the bear.
Unknown
inv-rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "needs" "bear" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "nice" "+")
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "round" "-")
The mouse needs the dog.
Unknown
rconc
[@2: The mouse needs the dog.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("mouse" "needs" "dog" "+")
The bear does not need the dog.
Unknown
inv-rconc
[@2: The bear needs the dog.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("bear" "needs" "dog" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "round" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The mouse likes the bear.
Unknown
random
[@0: The mouse likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bear" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The rabbit visits the dog.
Unknown
random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "+")
@0: The bear is green.[(triple1)] The dog is green.[(triple2)] The dog is rough.[(triple3)] The dog likes the mouse.[(triple4)] The dog likes the rabbit.[(triple5)] The dog visits the bear.[(triple6)] The mouse does not visit the dog.[(triple8)] The mouse is not blue.[(triple7)] The rabbit is nice.[(triple9)] The rabbit likes the dog.[(triple10)] The rabbit likes the mouse.[(triple11)] The rabbit visits the mouse.[(triple12)] @1: The mouse visits the rabbit.[(((triple11) -> rule4) OR ((triple4) -> rule4))] The rabbit is round.[(((triple12) -> rule6))] The rabbit needs the bear.[(((triple9) -> rule5))] @2: The mouse is nice.[(((((triple11) -> rule4)) -> rule1) OR ((((triple4) -> rule4)) -> rule1))] The rabbit needs the dog.[(((((triple12) -> rule6)) -> rule3))] @3: The dog visits the mouse.[(((((((triple12) -> rule6)) -> rule3) triple5) -> rule8))] The mouse needs the bear.[(((((((triple11) -> rule4)) -> rule1)) -> rule5) OR ((((((triple4) -> rule4)) -> rule1)) -> rule5))] @4: The dog is not nice.[(((triple2 ((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule2))] The dog is round.[(((((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule6))] @5: The dog needs the dog.[(((((((((((triple12) -> rule6)) -> rule3) triple5) -> rule8)) -> rule6)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple5
The dog visits the bear.
("dog" "visits" "bear" "+")
triple6
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
triple8
The mouse is not blue.
("mouse" "is" "blue" "-")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple10
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple11
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((triple11) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
((triple4) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple12) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((triple9) -> (rule5 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2)) triple5) -> (rule8 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
The dog is not nice.
("dog" "is" "nice" "-")
((triple2 ((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule2 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The dog is round.
("dog" "is" "round" "+")
((((((((triple12) -> (rule6 % int4))) -> (rule3 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((((((triple12) -> (rule6 % int5))) -> (rule3 % int4)) triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
int5