The bear is kind. The bear is red. The bear sees the dog. The bear sees the rabbit. The dog is red. The dog is young. The dog likes the lion. The dog needs the lion. The dog sees the rabbit. The lion is red. The lion needs the rabbit. The lion sees the dog. The rabbit is cold. The rabbit is red. The rabbit likes the dog. The rabbit sees the lion. If someone is cold then they see the lion. If someone is young and they need the dog then the dog is red. If the rabbit sees the bear and the bear sees the dog then the rabbit likes the bear. If the bear is red then the bear needs the dog. If someone needs the dog then they like the bear. If someone likes the bear and the bear is red then the bear likes the dog.
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone is cold then they see the lion.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "lion" "+"))
If someone is young and they need the dog then the dog is red.
((("someone" "is" "young" "+") ("someone" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
If the rabbit sees the bear and the bear sees the dog then the rabbit likes the bear.
((("rabbit" "sees" "bear" "+") ("bear" "sees" "dog" "+")) -> ("rabbit" "likes" "bear" "+"))
If the bear is red then the bear needs the dog.
((("bear" "is" "red" "+")) -> ("bear" "needs" "dog" "+"))
If someone needs the dog then they like the bear.
((("someone" "needs" "dog" "+")) -> ("someone" "likes" "bear" "+"))
If someone likes the bear and the bear is red then the bear likes the dog.
((("someone" "likes" "bear" "+") ("bear" "is" "red" "+")) -> ("bear" "likes" "dog" "+"))
The dog sees the rabbit.
True
1
proof
[(triple9)]
("dog" "sees" "rabbit" "+")
triple9
The rabbit does not like the dog.
False
1
inv-proof
[(triple15)]
("rabbit" "likes" "dog" "-")
triple15
The bear needs the dog.
True
2
proof
[(((triple2) -> rule4))]
("bear" "needs" "dog" "+")
((triple2) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear does not need the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("bear" "needs" "dog" "-")
((triple2) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear likes the bear.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("bear" "likes" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear does not like the bear.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("bear" "likes" "bear" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear likes the dog.
True
5
proof
[(((((((triple2) -> rule4)) -> rule5) triple2) -> rule6))]
("bear" "likes" "dog" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
int3
The bear does not like the dog.
False
5
inv-proof
[(((((((triple2) -> rule4)) -> rule5) triple2) -> rule6))]
("bear" "likes" "dog" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
int3
The rabbit does not like the bear.
Unknown
inv-rconc
[@1: The rabbit likes the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "bear" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "+")
The dog does not like the bear.
Unknown
inv-rconc
[@1: The dog likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "bear" "-")
The lion likes the bear.
Unknown
rconc
[@1: The lion likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "likes" "bear" "+")
The dog does not need the bear.
Unknown
inv-random
[@0: The dog needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bear" "-")
The rabbit sees the bear.
Unknown
random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is kind.[(triple1)] The bear is red.[(triple2)] The bear sees the dog.[(triple3)] The bear sees the rabbit.[(triple4)] The dog is red.[(triple5)] The dog is young.[(triple6)] The dog likes the lion.[(triple7)] The dog needs the lion.[(triple8)] The dog sees the rabbit.[(triple9)] The lion is red.[(triple10)] The lion needs the rabbit.[(triple11)] The lion sees the dog.[(triple12)] The rabbit is cold.[(triple13)] The rabbit is red.[(triple14)] The rabbit likes the dog.[(triple15)] The rabbit sees the lion.[(triple16 OR ((triple13) -> rule1))] @1: The bear needs the dog.[(((triple2) -> rule4))] @2: The bear likes the bear.[(((((triple2) -> rule4)) -> rule5))] @3: The bear likes the dog.[(((((((triple2) -> rule4)) -> rule5) triple2) -> rule6))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog likes the lion.
("dog" "likes" "lion" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple9
The lion is red.
("lion" "is" "red" "+")
triple10
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple11
The lion sees the dog.
("lion" "sees" "dog" "+")
triple12
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple13
The rabbit is red.
("rabbit" "is" "red" "+")
triple14
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple15
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple16
((triple13) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
((triple2) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
int3