The bear is green. The bear is rough. The bear sees the dog. The bear sees the tiger. The bear visits the cat. The cat is red. The cat likes the tiger. The cat sees the dog. The dog likes the bear. The dog likes the tiger. The dog sees the bear. The dog sees the tiger. The dog visits the cat. The tiger likes the bear. The tiger likes the dog. The tiger visits the cat. If something is rough then it likes the cat. If something likes the bear and it is red then the bear is young. If something visits the dog then the dog likes the bear. If something sees the cat and the cat is nice then it is green. If the dog visits the bear then the dog likes the cat. If something sees the bear and the bear likes the cat then the cat is rough. If something is red and it likes the cat then it likes the bear. If something sees the bear and the bear likes the cat then the cat visits the tiger. If something is red and it likes the cat then the cat is nice.
The bear is green.
("bear" "is" "green" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something is rough then it likes the cat.
((("something" "is" "rough" "+")) -> ("something" "likes" "cat" "+"))
If something likes the bear and it is red then the bear is young.
((("something" "likes" "bear" "+") ("something" "is" "red" "+")) -> ("bear" "is" "young" "+"))
If something visits the dog then the dog likes the bear.
((("something" "visits" "dog" "+")) -> ("dog" "likes" "bear" "+"))
If something sees the cat and the cat is nice then it is green.
((("something" "sees" "cat" "+") ("cat" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If the dog visits the bear then the dog likes the cat.
((("dog" "visits" "bear" "+")) -> ("dog" "likes" "cat" "+"))
If something sees the bear and the bear likes the cat then the cat is rough.
((("something" "sees" "bear" "+") ("bear" "likes" "cat" "+")) -> ("cat" "is" "rough" "+"))
If something is red and it likes the cat then it likes the bear.
((("something" "is" "red" "+") ("something" "likes" "cat" "+")) -> ("something" "likes" "bear" "+"))
If something sees the bear and the bear likes the cat then the cat visits the tiger.
((("something" "sees" "bear" "+") ("bear" "likes" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If something is red and it likes the cat then the cat is nice.
((("something" "is" "red" "+") ("something" "likes" "cat" "+")) -> ("cat" "is" "nice" "+"))
The dog likes the tiger.
True
1
proof
[(triple10)]
("dog" "likes" "tiger" "+")
triple10
The dog does not like the bear.
False
1
inv-proof
[(triple9)]
("dog" "likes" "bear" "-")
triple9
The bear likes the cat.
True
2
proof
[(((triple2) -> rule1))]
("bear" "likes" "cat" "+")
((triple2) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear does not like the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "likes" "cat" "-")
((triple2) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat is rough.
True
4
proof
[(((triple11 ((triple2) -> rule1)) -> rule6))]
("cat" "is" "rough" "+")
((triple11 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat does not visit the tiger.
False
4
inv-proof
[(((triple11 ((triple2) -> rule1)) -> rule8))]
("cat" "visits" "tiger" "-")
((triple11 ((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat likes the cat.
True
5
proof
[(((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1))]
("cat" "likes" "cat" "+")
((((triple11 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat does not like the cat.
False
5
inv-proof
[(((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1))]
("cat" "likes" "cat" "-")
((((triple11 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat likes the bear.
True
7
proof
[(((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule7))]
("cat" "likes" "bear" "+")
((triple6 ((((triple11 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The cat is not nice.
False
7
inv-proof
[(((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule9))]
("cat" "is" "nice" "-")
((triple6 ((((triple11 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bear is young.
True
9
proof
[(((((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule7) triple6) -> rule2))]
("bear" "is" "young" "+")
((((triple6 ((((triple11 ((triple2) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple6) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The bear likes the cat.
("bear" "likes" "cat" "+")
int5
The bear is not young.
False
9
inv-proof
[(((((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule7) triple6) -> rule2))]
("bear" "is" "young" "-")
((((triple6 ((((triple11 ((triple2) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple6) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The bear likes the cat.
("bear" "likes" "cat" "+")
int5
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "green" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "bear" "+")
The tiger does not like the cat.
Unknown
inv-rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "cat" "-")
The dog likes the cat.
Unknown
rconc
[@1: The dog likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "cat" "+")
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "green" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "green" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The tiger sees the cat.
Unknown
random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "+")
The cat does not visit the dog.
Unknown
inv-random
[@0: The cat visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "dog" "-")
The tiger sees the bear.
Unknown
random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear likes the dog.
Unknown
random
[@0: The bear likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "dog" "+")
@0: The bear is green.[(triple1)] The bear is rough.[(triple2)] The bear sees the dog.[(triple3)] The bear sees the tiger.[(triple4)] The bear visits the cat.[(triple5)] The cat is red.[(triple6)] The cat likes the tiger.[(triple7)] The cat sees the dog.[(triple8)] The dog likes the bear.[(triple9)] The dog likes the tiger.[(triple10)] The dog sees the bear.[(triple11)] The dog sees the tiger.[(triple12)] The dog visits the cat.[(triple13)] The tiger likes the bear.[(triple14)] The tiger likes the dog.[(triple15)] The tiger visits the cat.[(triple16)] @1: The bear likes the cat.[(((triple2) -> rule1))] @2: The cat is rough.[(((triple11 ((triple2) -> rule1)) -> rule6))] The cat visits the tiger.[(((triple11 ((triple2) -> rule1)) -> rule8))] @3: The cat likes the cat.[(((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1))] @4: The cat is nice.[(((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule9))] The cat likes the bear.[(((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule7))] @5: The bear is young.[(((((triple6 ((((triple11 ((triple2) -> rule1)) -> rule6)) -> rule1)) -> rule7) triple6) -> rule2))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The bear visits the cat.
("bear" "visits" "cat" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple7
The cat sees the dog.
("cat" "sees" "dog" "+")
triple8
The dog likes the bear.
("dog" "likes" "bear" "+")
triple9
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple10
The dog sees the bear.
("dog" "sees" "bear" "+")
triple11
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple12
The dog visits the cat.
("dog" "visits" "cat" "+")
triple13
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple14
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple15
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16
The bear likes the cat.
("bear" "likes" "cat" "+")
((triple2) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((triple11 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple11 ((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple11 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
((triple6 ((((triple11 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple6 ((((triple11 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bear is young.
("bear" "is" "young" "+")
((((triple6 ((((triple11 ((triple2) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple6) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The bear likes the cat.
("bear" "likes" "cat" "+")
int5