The bear is red. The bear is rough. The bear needs the rabbit. The cat is not blue. The cat is red. The cat is rough. The cat likes the tiger. The cat needs the bear. The cat needs the rabbit. The rabbit needs the bear. The tiger is cold. The tiger is rough. The tiger likes the rabbit. The tiger needs the rabbit. The tiger sees the rabbit. If the rabbit sees the bear then the bear is cold. If the rabbit likes the bear and the tiger does not see the rabbit then the tiger likes the cat. If someone is red then they do not need the tiger. If someone needs the tiger and the tiger sees the rabbit then the tiger needs the bear. If someone needs the bear then they are rough. If the cat likes the bear then the bear does not like the cat. If someone needs the cat and the cat needs the bear then they are blue. If the rabbit does not need the tiger then the rabbit is not cold.
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The cat is not blue.
("cat" "is" "blue" "-")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If the rabbit sees the bear then the bear is cold.
((("rabbit" "sees" "bear" "+")) -> ("bear" "is" "cold" "+"))
If the rabbit likes the bear and the tiger does not see the rabbit then the tiger likes the cat.
((("rabbit" "likes" "bear" "+") ("tiger" "sees" "rabbit" "~")) -> ("tiger" "likes" "cat" "+"))
If someone is red then they do not need the tiger.
((("someone" "is" "red" "+")) -> ("someone" "needs" "tiger" "-"))
If someone needs the tiger and the tiger sees the rabbit then the tiger needs the bear.
((("someone" "needs" "tiger" "+") ("tiger" "sees" "rabbit" "+")) -> ("tiger" "needs" "bear" "+"))
If someone needs the bear then they are rough.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "rough" "+"))
If the cat likes the bear then the bear does not like the cat.
((("cat" "likes" "bear" "+")) -> ("bear" "likes" "cat" "-"))
If someone needs the cat and the cat needs the bear then they are blue.
((("someone" "needs" "cat" "+") ("cat" "needs" "bear" "+")) -> ("someone" "is" "blue" "+"))
If the rabbit does not need the tiger then the rabbit is not cold.
((("rabbit" "needs" "tiger" "~")) -> ("rabbit" "is" "cold" "-"))
The tiger is cold.
True
1
proof
[(triple11)]
("tiger" "is" "cold" "+")
triple11
The cat does not need the rabbit.
False
1
inv-proof
[(triple9)]
("cat" "needs" "rabbit" "-")
triple9
The bear does not need the tiger.
True
2
proof
[(((triple1) -> rule3))]
("bear" "needs" "tiger" "-")
((triple1) -> (rule3 % int1))
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
int1
The bear needs the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
int1
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "blue" "-")
The tiger likes the cat.
Unknown
rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "cat" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The cat sees the tiger.
Unknown
random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "+")
@0: The bear is red.[(triple1)] The bear is rough.[(triple2)] The bear needs the rabbit.[(triple3)] The cat is not blue.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6 OR ((triple8) -> rule5))] The cat likes the tiger.[(triple7)] The cat needs the bear.[(triple8)] The cat needs the rabbit.[(triple9)] The rabbit needs the bear.[(triple10)] The tiger is cold.[(triple11)] The tiger is rough.[(triple12)] The tiger likes the rabbit.[(triple13)] The tiger needs the rabbit.[(triple14)] The tiger sees the rabbit.[(triple15)] @1: The bear does not need the tiger.[(((triple1) -> rule3))] The cat does not need the tiger.[(((triple5) -> rule3))] The rabbit is rough.[(((triple10) -> rule5))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple3
The cat is not blue.
("cat" "is" "blue" "-")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
((triple8) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple7
The cat needs the bear.
("cat" "needs" "bear" "+")
triple8
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple9
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple13
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple14
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple15
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
((triple1) -> (rule3 % int1))
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
int1
The cat does not need the tiger.
("cat" "needs" "tiger" "-")
((triple5) -> (rule3 % int1))
The cat does not need the tiger.
("cat" "needs" "tiger" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple10) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1