The bear is big. The cow needs the bear. The cow sees the squirrel. The squirrel does not eat the tiger. The squirrel needs the cow. The tiger is big. The tiger is young. If something is young and it needs the cow then it does not need the tiger. If something eats the bear and it needs the squirrel then the squirrel sees the tiger. If something is young then it needs the cow.
The bear is big.
("bear" "is" "big" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
If something is young and it needs the cow then it does not need the tiger.
((("something" "is" "young" "+") ("something" "needs" "cow" "+")) -> ("something" "needs" "tiger" "-"))
If something eats the bear and it needs the squirrel then the squirrel sees the tiger.
((("something" "eats" "bear" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "+"))
If something is young then it needs the cow.
((("something" "is" "young" "+")) -> ("something" "needs" "cow" "+"))
The bear is big.
True
1
proof
[(triple1)]
("bear" "is" "big" "+")
triple1
The cow does not need the bear.
False
1
inv-proof
[(triple2)]
("cow" "needs" "bear" "-")
triple2
The tiger needs the cow.
True
2
proof
[(((triple7) -> rule3))]
("tiger" "needs" "cow" "+")
((triple7) -> (rule3 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the cow.
False
2
inv-proof
[(((triple7) -> rule3))]
("tiger" "needs" "cow" "-")
((triple7) -> (rule3 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the tiger.
True
4
proof
[(((triple7 ((triple7) -> rule3)) -> rule1))]
("tiger" "needs" "tiger" "-")
((triple7 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
False
4
inv-proof
[(((triple7 ((triple7) -> rule3)) -> rule1))]
("tiger" "needs" "tiger" "+")
((triple7 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The bear does not need the cow.
Unknown
inv-rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "cow" "-")
The squirrel sees the tiger.
Unknown
rconc
[@1: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "tiger" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear eats the squirrel.
Unknown
random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "+")
@0: The bear is big.[(triple1)] The cow needs the bear.[(triple2)] The cow sees the squirrel.[(triple3)] The squirrel does not eat the tiger.[(triple4)] The squirrel needs the cow.[(triple5)] The tiger is big.[(triple6)] The tiger is young.[(triple7)] @1: The tiger needs the cow.[(((triple7) -> rule3))] @2: The tiger does not need the tiger.[(((triple7 ((triple7) -> rule3)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The cow needs the bear.
("cow" "needs" "bear" "+")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple3
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
triple4
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger is young.
("tiger" "is" "young" "+")
triple7
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple7) -> (rule3 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
((triple7 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2