The bear is rough. The bear sees the dog. The dog eats the tiger. The dog needs the bear. The lion is red. The tiger is blue. The tiger is green. If someone is blue then they need the bear.
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The lion is red.
("lion" "is" "red" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone is blue then they need the bear.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "bear" "+"))
The tiger is blue.
True
1
proof
[(triple6)]
("tiger" "is" "blue" "+")
triple6
The dog does not eat the tiger.
False
1
inv-proof
[(triple3)]
("dog" "eats" "tiger" "-")
triple3
The tiger needs the bear.
True
2
proof
[(((triple6) -> rule1))]
("tiger" "needs" "bear" "+")
((triple6) -> (rule1 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger does not need the bear.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "needs" "bear" "-")
((triple6) -> (rule1 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "-")
The lion needs the bear.
Unknown
rconc
[@1: The lion needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "bear" "+")
The lion does not see the tiger.
Unknown
inv-random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The bear is rough.[(triple1)] The bear sees the dog.[(triple2)] The dog eats the tiger.[(triple3)] The dog needs the bear.[(triple4)] The lion is red.[(triple5)] The tiger is blue.[(triple6)] The tiger is green.[(triple7)] @1: The tiger needs the bear.[(((triple6) -> rule1))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple3
The dog needs the bear.
("dog" "needs" "bear" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((triple6) -> (rule1 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1