The bear is big. The bear sees the cat. The cat is big. The cat is rough. The cat likes the bear. The cat needs the bear. The cat sees the bear. If someone needs the bear and the bear is green then the bear needs the cat. If the cat needs the bear and the bear sees the cat then the bear is green. If someone needs the bear then the bear sees the cat.
The bear is big.
("bear" "is" "big" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
If someone needs the bear and the bear is green then the bear needs the cat.
((("someone" "needs" "bear" "+") ("bear" "is" "green" "+")) -> ("bear" "needs" "cat" "+"))
If the cat needs the bear and the bear sees the cat then the bear is green.
((("cat" "needs" "bear" "+") ("bear" "sees" "cat" "+")) -> ("bear" "is" "green" "+"))
If someone needs the bear then the bear sees the cat.
((("someone" "needs" "bear" "+")) -> ("bear" "sees" "cat" "+"))
The cat is big.
True
1
proof
[(triple3)]
("cat" "is" "big" "+")
triple3
The cat is not big.
False
1
inv-proof
[(triple3)]
("cat" "is" "big" "-")
triple3
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is big.[(triple1)] The bear sees the cat.[(triple2 OR ((triple6) -> rule3))] The cat is big.[(triple3)] The cat is rough.[(triple4)] The cat likes the bear.[(triple5)] The cat needs the bear.[(triple6)] The cat sees the bear.[(triple7)] @1: The bear is green.[(((triple6 triple2) -> rule2) OR ((triple6 ((triple6) -> rule3)) -> rule2))] @2: The bear needs the cat.[(((triple6 ((triple6 triple2) -> rule2)) -> rule1) OR ((triple6 ((triple6 ((triple6) -> rule3)) -> rule2)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear sees the cat.
("bear" "sees" "cat" "+")
triple2
((triple6) -> (rule3 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat likes the bear.
("cat" "likes" "bear" "+")
triple5
The cat needs the bear.
("cat" "needs" "bear" "+")
triple6
The cat sees the bear.
("cat" "sees" "bear" "+")
triple7
The bear is green.
("bear" "is" "green" "+")
((triple6 triple2) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The bear needs the cat.
("bear" "needs" "cat" "+")
((triple6 ((triple6 triple2) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((triple6 ((triple6 ((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3