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