The bear chases the cat. The cat is blue. The cat likes the tiger. The cat needs the tiger. The tiger is big. The tiger likes the bear. The tiger likes the cat. If someone needs the bear then the bear chases the cat. If someone likes the bear then the bear needs the tiger. If someone needs the cat then the cat likes the tiger. If someone likes the bear then they like the cat. If the cat chases the bear then the bear likes the tiger. If someone needs the bear then the bear likes the cat.
The bear chases the cat.
("bear" "chases" "cat" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If someone needs the bear then the bear chases the cat.
((("someone" "needs" "bear" "+")) -> ("bear" "chases" "cat" "+"))
If someone likes the bear then the bear needs the tiger.
((("someone" "likes" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If someone needs the cat then the cat likes the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
If someone likes the bear then they like the cat.
((("someone" "likes" "bear" "+")) -> ("someone" "likes" "cat" "+"))
If the cat chases the bear then the bear likes the tiger.
((("cat" "chases" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
If someone needs the bear then the bear likes the cat.
((("someone" "needs" "bear" "+")) -> ("bear" "likes" "cat" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The bear does not chase the cat.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cat" "-")
triple1
The bear needs the tiger.
True
2
proof
[(((triple6) -> rule2))]
("bear" "needs" "tiger" "+")
((triple6) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear does not need the tiger.
False
2
inv-proof
[(((triple6) -> rule2))]
("bear" "needs" "tiger" "-")
((triple6) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "cat" "-")
The bear likes the cat.
Unknown
rconc
[@1: The bear likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "cat" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear chases the cat.[(triple1)] The cat is blue.[(triple2)] The cat likes the tiger.[(triple3)] The cat needs the tiger.[(triple4)] The tiger is big.[(triple5)] The tiger likes the bear.[(triple6)] The tiger likes the cat.[(triple7 OR ((triple6) -> rule4))] @1: The bear needs the tiger.[(((triple6) -> rule2))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple6
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
((triple6) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple6) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1