The bear does not eat the cat. The bear is big. The bear is rough. The bear sees the cat. The cat eats the bear. The cat eats the tiger. The cat is not green. The cat needs the bear. The tiger eats the bear. The tiger is green. The tiger is rough. The tiger is round. The tiger needs the bear. The tiger needs the cat. The tiger sees the bear. The tiger sees the cat. If the bear sees the cat and the bear does not eat the cat then the cat is round. If something needs the cat then it is rough.
The bear does not eat the cat.
("bear" "eats" "cat" "-")
The bear is big.
("bear" "is" "big" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat needs the bear.
("cat" "needs" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the bear sees the cat and the bear does not eat the cat then the cat is round.
((("bear" "sees" "cat" "+") ("bear" "eats" "cat" "~")) -> ("cat" "is" "round" "+"))
If something needs the cat then it is rough.
((("something" "needs" "cat" "+")) -> ("something" "is" "rough" "+"))
The bear does not eat the cat.
True
1
proof
[(triple1)]
("bear" "eats" "cat" "-")
triple1
The tiger does not see the bear.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "bear" "-")
triple15
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "rough" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The bear does not eat the cat.[(triple1)] The bear is big.[(triple2)] The bear is rough.[(triple3)] The bear sees the cat.[(triple4)] The cat eats the bear.[(triple5)] The cat eats the tiger.[(triple6)] The cat is not green.[(triple7)] The cat needs the bear.[(triple8)] The tiger eats the bear.[(triple9)] The tiger is green.[(triple10)] The tiger is rough.[(triple11 OR ((triple14) -> rule2))] The tiger is round.[(triple12)] The tiger needs the bear.[(triple13)] The tiger needs the cat.[(triple14)] The tiger sees the bear.[(triple15)] The tiger sees the cat.[(triple16)] @1: The cat is round.[(((triple4 triple1) -> rule1))]
The bear does not eat the cat.
("bear" "eats" "cat" "-")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The cat eats the bear.
("cat" "eats" "bear" "+")
triple5
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple6
The cat is not green.
("cat" "is" "green" "-")
triple7
The cat needs the bear.
("cat" "needs" "bear" "+")
triple8
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
((triple14) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple13
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple14
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple15
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple16
The cat is round.
("cat" "is" "round" "+")
((triple4 triple1) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1