The bear likes the dog. The bear likes the tiger. The bear sees the rabbit. The dog is nice. The dog likes the tiger. The dog needs the tiger. The rabbit does not like the dog. The tiger is green. The tiger is not kind. The tiger is red. The tiger needs the rabbit. If someone needs the tiger then they like the rabbit. If someone sees the rabbit then the rabbit sees the bear. If someone likes the rabbit and the rabbit is rough then the rabbit does not like the tiger. If someone needs the bear and they are nice then they need the tiger. If someone needs the bear then the bear needs the tiger. If the tiger needs the rabbit then the tiger needs the bear. If someone is green and they need the rabbit then the rabbit likes the bear. If someone is red and they like the dog then they need the dog. If someone likes the rabbit then they are red.
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The rabbit does not like the dog.
("rabbit" "likes" "dog" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If someone needs the tiger then they like the rabbit.
((("someone" "needs" "tiger" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone sees the rabbit then the rabbit sees the bear.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "bear" "+"))
If someone likes the rabbit and the rabbit is rough then the rabbit does not like the tiger.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "likes" "tiger" "-"))
If someone needs the bear and they are nice then they need the tiger.
((("someone" "needs" "bear" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the bear then the bear needs the tiger.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If the tiger needs the rabbit then the tiger needs the bear.
((("tiger" "needs" "rabbit" "+")) -> ("tiger" "needs" "bear" "+"))
If someone is green and they need the rabbit then the rabbit likes the bear.
((("someone" "is" "green" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "likes" "bear" "+"))
If someone is red and they like the dog then they need the dog.
((("someone" "is" "red" "+") ("someone" "likes" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If someone likes the rabbit then they are red.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "red" "+"))
The dog needs the tiger.
True
1
proof
[(triple6)]
("dog" "needs" "tiger" "+")
triple6
The dog is not nice.
False
1
inv-proof
[(triple4)]
("dog" "is" "nice" "-")
triple4
The dog likes the rabbit.
True
2
proof
[(((triple6) -> rule1))]
("dog" "likes" "rabbit" "+")
((triple6) -> (rule1 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The tiger does not need the bear.
False
2
inv-proof
[(((triple11) -> rule6))]
("tiger" "needs" "bear" "-")
((triple11) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The dog is red.
True
3
proof
[(((((triple6) -> rule1)) -> rule9))]
("dog" "is" "red" "+")
((((triple6) -> (rule1 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog is not red.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule9))]
("dog" "is" "red" "-")
((((triple6) -> (rule1 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The bear likes the rabbit.
True
4
proof
[(((((((triple11) -> rule6)) -> rule5)) -> rule1))]
("bear" "likes" "rabbit" "+")
((((((triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The bear does not like the rabbit.
False
4
inv-proof
[(((((((triple11) -> rule6)) -> rule5)) -> rule1))]
("bear" "likes" "rabbit" "-")
((((((triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The bear is red.
True
5
proof
[(((((((((triple11) -> rule6)) -> rule5)) -> rule1)) -> rule9))]
("bear" "is" "red" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The bear is not red.
False
5
inv-proof
[(((((((((triple11) -> rule6)) -> rule5)) -> rule1)) -> rule9))]
("bear" "is" "red" "-")
((((((((triple11) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The bear needs the dog.
True
7
proof
[(((((((((((triple11) -> rule6)) -> rule5)) -> rule1)) -> rule9) triple1) -> rule8))]
("bear" "needs" "dog" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule9 % int2)) triple1) -> (rule8 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5
The bear does not need the dog.
False
7
inv-proof
[(((((((((((triple11) -> rule6)) -> rule5)) -> rule1)) -> rule9) triple1) -> rule8))]
("bear" "needs" "dog" "-")
((((((((((triple11) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule9 % int2)) triple1) -> (rule8 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "needs" "dog" "-")
The tiger likes the rabbit.
Unknown
rconc
[@2: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("tiger" "likes" "rabbit" "+")
The rabbit is not red.
Unknown
inv-rconc
[@3: The rabbit is red.[CWA. Example of deepest failure = (rule9 <- rule1 <- rule4 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit needs the tiger.
Unknown
rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "needs" "tiger" "+")
The rabbit does not need the dog.
Unknown
inv-rconc
[@1: The rabbit needs the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "needs" "dog" "-")
The tiger needs the dog.
Unknown
rconc
[@1: The tiger needs the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "dog" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The rabbit likes the tiger.
Unknown
random
[@0: The rabbit likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "tiger" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The bear likes the dog.[(triple1)] The bear likes the tiger.[(triple2)] The bear sees the rabbit.[(triple3)] The dog is nice.[(triple4)] The dog likes the tiger.[(triple5)] The dog needs the tiger.[(triple6)] The rabbit does not like the dog.[(triple7)] The tiger is green.[(triple8)] The tiger is not kind.[(triple9)] The tiger is red.[(triple10)] The tiger needs the rabbit.[(triple11)] @1: The dog likes the rabbit.[(((triple6) -> rule1))] The rabbit likes the bear.[(((triple8 triple11) -> rule7))] The rabbit sees the bear.[(((triple3) -> rule2))] The tiger needs the bear.[(((triple11) -> rule6))] @2: The bear needs the tiger.[(((((triple11) -> rule6)) -> rule5))] The dog is red.[(((((triple6) -> rule1)) -> rule9))] @3: The bear likes the rabbit.[(((((((triple11) -> rule6)) -> rule5)) -> rule1))] @4: The bear is red.[(((((((((triple11) -> rule6)) -> rule5)) -> rule1)) -> rule9))] @5: The bear needs the dog.[(((((((((((triple11) -> rule6)) -> rule5)) -> rule1)) -> rule9) triple1) -> rule8))]
The bear likes the dog.
("bear" "likes" "dog" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The rabbit does not like the dog.
("rabbit" "likes" "dog" "-")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is not kind.
("tiger" "is" "kind" "-")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
((triple6) -> (rule1 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((triple8 triple11) -> (rule7 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
((triple3) -> (rule2 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((triple11) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((triple11) -> (rule6 % int2))) -> (rule5 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The dog is red.
("dog" "is" "red" "+")
((((triple6) -> (rule1 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
((((((triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The bear is red.
("bear" "is" "red" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The bear needs the dog.
("bear" "needs" "dog" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule9 % int2)) triple1) -> (rule8 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5