The dog chases the mouse. The dog eats the rabbit. The dog is nice. The dog is young. The dog likes the rabbit. The mouse chases the dog. The mouse eats the rabbit. The mouse is nice. The rabbit chases the dog. The rabbit chases the mouse. The rabbit eats the dog. The rabbit eats the mouse. The rabbit is red. The rabbit is rough. The rabbit is young. The rabbit likes the dog. If something is kind and young then it likes the rabbit. If something chases the mouse then the mouse is young. If something chases the dog and it likes the rabbit then the dog eats the mouse. If something eats the rabbit and the rabbit eats the mouse then the mouse is kind. If the rabbit chases the dog then the rabbit is rough. If something chases the dog and it is nice then the dog chases the rabbit. If something eats the dog and the dog is red then the dog likes the mouse. If something likes the mouse then it eats the mouse.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
If something is kind and young then it likes the rabbit.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "likes" "rabbit" "+"))
If something chases the mouse then the mouse is young.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something chases the dog and it likes the rabbit then the dog eats the mouse.
((("something" "chases" "dog" "+") ("something" "likes" "rabbit" "+")) -> ("dog" "eats" "mouse" "+"))
If something eats the rabbit and the rabbit eats the mouse then the mouse is kind.
((("something" "eats" "rabbit" "+") ("rabbit" "eats" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the rabbit chases the dog then the rabbit is rough.
((("rabbit" "chases" "dog" "+")) -> ("rabbit" "is" "rough" "+"))
If something chases the dog and it is nice then the dog chases the rabbit.
((("something" "chases" "dog" "+") ("something" "is" "nice" "+")) -> ("dog" "chases" "rabbit" "+"))
If something eats the dog and the dog is red then the dog likes the mouse.
((("something" "eats" "dog" "+") ("dog" "is" "red" "+")) -> ("dog" "likes" "mouse" "+"))
If something likes the mouse then it eats the mouse.
((("something" "likes" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
The rabbit is rough.
True
1
proof
[(triple14 OR ((triple9) -> rule5))]
("rabbit" "is" "rough" "+")
triple14
((triple9) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit does not like the dog.
False
1
inv-proof
[(triple16)]
("rabbit" "likes" "dog" "-")
triple16
The mouse is young.
True
2
proof
[(((triple1) -> rule2) OR ((triple10) -> rule2))]
("mouse" "is" "young" "+")
((triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple10) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The dog does not chase the rabbit.
False
3
inv-proof
[(((triple6 triple8) -> rule6))]
("dog" "chases" "rabbit" "-")
((triple6 triple8) -> (rule6 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The mouse likes the rabbit.
True
6
proof
[(((((triple2 triple12) -> rule4) ((triple1) -> rule2)) -> rule1) OR ((((triple2 triple12) -> rule4) ((triple10) -> rule2)) -> rule1) OR ((((triple7 triple12) -> rule4) ((triple1) -> rule2)) -> rule1) OR ((((triple7 triple12) -> rule4) ((triple10) -> rule2)) -> rule1))]
("mouse" "likes" "rabbit" "+")
((((triple2 triple12) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple2 triple12) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple7 triple12) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple7 triple12) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse does not like the rabbit.
False
6
inv-proof
[(((((triple2 triple12) -> rule4) ((triple1) -> rule2)) -> rule1) OR ((((triple2 triple12) -> rule4) ((triple10) -> rule2)) -> rule1) OR ((((triple7 triple12) -> rule4) ((triple1) -> rule2)) -> rule1) OR ((((triple7 triple12) -> rule4) ((triple10) -> rule2)) -> rule1))]
("mouse" "likes" "rabbit" "-")
((((triple2 triple12) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple2 triple12) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple7 triple12) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple7 triple12) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The dog eats the mouse.
True
8
proof
[(((triple6 ((((triple2 triple12) -> rule4) ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple2 triple12) -> rule4) ((triple10) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple12) -> rule4) ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple12) -> rule4) ((triple10) -> rule2)) -> rule1)) -> rule3))]
("dog" "eats" "mouse" "+")
((triple6 ((((triple2 triple12) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple2 triple12) -> (rule4 % int4)) ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple7 triple12) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple7 triple12) -> (rule4 % int4)) ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The dog does not eat the mouse.
False
8
inv-proof
[(((triple6 ((((triple2 triple12) -> rule4) ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple2 triple12) -> rule4) ((triple10) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple12) -> rule4) ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple12) -> rule4) ((triple10) -> rule2)) -> rule1)) -> rule3))]
("dog" "eats" "mouse" "-")
((triple6 ((((triple2 triple12) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple2 triple12) -> (rule4 % int4)) ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple7 triple12) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple7 triple12) -> (rule4 % int4)) ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The dog likes the mouse.
Unknown
rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "likes" "mouse" "+")
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit does not like the mouse.
Unknown
inv-random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog chases the mouse.[(triple1)] The dog eats the rabbit.[(triple2)] The dog is nice.[(triple3)] The dog is young.[(triple4)] The dog likes the rabbit.[(triple5)] The mouse chases the dog.[(triple6)] The mouse eats the rabbit.[(triple7)] The mouse is nice.[(triple8)] The rabbit chases the dog.[(triple9)] The rabbit chases the mouse.[(triple10)] The rabbit eats the dog.[(triple11)] The rabbit eats the mouse.[(triple12)] The rabbit is red.[(triple13)] The rabbit is rough.[(triple14 OR ((triple9) -> rule5))] The rabbit is young.[(triple15)] The rabbit likes the dog.[(triple16)] @1: The dog chases the rabbit.[(((triple6 triple8) -> rule6))] The mouse is kind.[(((triple2 triple12) -> rule4) OR ((triple7 triple12) -> rule4))] The mouse is young.[(((triple1) -> rule2) OR ((triple10) -> rule2))] @2: The mouse likes the rabbit.[(((((triple2 triple12) -> rule4) ((triple1) -> rule2)) -> rule1) OR ((((triple2 triple12) -> rule4) ((triple10) -> rule2)) -> rule1) OR ((((triple7 triple12) -> rule4) ((triple1) -> rule2)) -> rule1) OR ((((triple7 triple12) -> rule4) ((triple10) -> rule2)) -> rule1))] @3: The dog eats the mouse.[(((triple6 ((((triple2 triple12) -> rule4) ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple2 triple12) -> rule4) ((triple10) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple12) -> rule4) ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple12) -> rule4) ((triple10) -> rule2)) -> rule1)) -> rule3))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple5
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple6
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple9
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple10
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple11
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple13
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple14
((triple9) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple15
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple16
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((triple6 triple8) -> (rule6 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2 triple12) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((triple7 triple12) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple10) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple2 triple12) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple2 triple12) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple7 triple12) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((triple7 triple12) -> (rule4 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple6 ((((triple2 triple12) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple2 triple12) -> (rule4 % int4)) ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple7 triple12) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((triple6 ((((triple7 triple12) -> (rule4 % int4)) ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4