The bear sees the cat. The cat does not see the bear. The cow needs the bear. If something needs the bear and the bear is green then the bear eats the cat. If something sees the cat then the cat sees the cow. If something sees the cow then it needs the cat.
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat does not see the bear.
("cat" "sees" "bear" "-")
The cow needs the bear.
("cow" "needs" "bear" "+")
If something needs the bear and the bear is green then the bear eats the cat.
((("something" "needs" "bear" "+") ("bear" "is" "green" "+")) -> ("bear" "eats" "cat" "+"))
If something sees the cat then the cat sees the cow.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "cow" "+"))
If something sees the cow then it needs the cat.
((("something" "sees" "cow" "+")) -> ("something" "needs" "cat" "+"))
The cow needs the bear.
True
1
proof
[(triple3)]
("cow" "needs" "bear" "+")
triple3
The bear does not see the cat.
False
1
inv-proof
[(triple1)]
("bear" "sees" "cat" "-")
triple1
The cat sees the cow.
True
2
proof
[(((triple1) -> rule2))]
("cat" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat does not see the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "sees" "cow" "-")
((triple1) -> (rule2 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat needs the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("cat" "needs" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat does not need the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("cat" "needs" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The bear does not need the cat.
Unknown
inv-rconc
[@1: The bear needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "cat" "-")
The bear eats the cat.
Unknown
rconc
[@1: The bear eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "cat" "+")
The cow does not need the cat.
Unknown
inv-rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cat" "-")
The cat needs the cow.
Unknown
random
[@0: The cat needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cow" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bear sees the cat.[(triple1)] The cat does not see the bear.[(triple2)] The cow needs the bear.[(triple3)] @1: The cat sees the cow.[(((triple1) -> rule2))] @2: The cat needs the cat.[(((((triple1) -> rule2)) -> rule3))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
The cat does not see the bear.
("cat" "sees" "bear" "-")
triple2
The cow needs the bear.
("cow" "needs" "bear" "+")
triple3
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2