The bear is big. The bear needs the mouse. The bear sees the dog. The dog is round. The dog sees the mouse. The mouse chases the dog. The mouse is big. The mouse needs the tiger. The tiger needs the bear. The tiger sees the dog. All big people are red. If someone needs the mouse then the mouse sees the tiger. If the tiger needs the mouse then the tiger chases the mouse. If someone sees the dog then they are nice. If someone is blue then they chase the bear. If someone is red and they need the tiger then they chase the bear. If someone is round then they need the tiger. If someone sees the bear and they are round then the bear chases the mouse.
The bear is big.
("bear" "is" "big" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
All big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone needs the mouse then the mouse sees the tiger.
((("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
If the tiger needs the mouse then the tiger chases the mouse.
((("tiger" "needs" "mouse" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone sees the dog then they are nice.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue then they chase the bear.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "bear" "+"))
If someone is red and they need the tiger then they chase the bear.
((("someone" "is" "red" "+") ("someone" "needs" "tiger" "+")) -> ("someone" "chases" "bear" "+"))
If someone is round then they need the tiger.
((("someone" "is" "round" "+")) -> ("someone" "needs" "tiger" "+"))
If someone sees the bear and they are round then the bear chases the mouse.
((("someone" "sees" "bear" "+") ("someone" "is" "round" "+")) -> ("bear" "chases" "mouse" "+"))
The tiger sees the dog.
True
1
proof
[(triple10)]
("tiger" "sees" "dog" "+")
triple10
The tiger does not see the dog.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "dog" "-")
triple10
The dog needs the tiger.
True
2
proof
[(((triple4) -> rule7))]
("dog" "needs" "tiger" "+")
((triple4) -> (rule7 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple7) -> rule1))]
("mouse" "is" "red" "-")
((triple7) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The bear does not chase the bear.
Unknown
inv-rconc
[@2: The bear chases the bear.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("bear" "chases" "bear" "-")
The bear needs the tiger.
Unknown
rconc
[@1: The bear needs the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "needs" "tiger" "+")
The bear does not need the dog.
Unknown
inv-random
[@0: The bear needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "dog" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The bear is big.[(triple1)] The bear needs the mouse.[(triple2)] The bear sees the dog.[(triple3)] The dog is round.[(triple4)] The dog sees the mouse.[(triple5)] The mouse chases the dog.[(triple6)] The mouse is big.[(triple7)] The mouse needs the tiger.[(triple8)] The tiger needs the bear.[(triple9)] The tiger sees the dog.[(triple10)] @1: The bear is nice.[(((triple3) -> rule4))] The bear is red.[(((triple1) -> rule1))] The dog needs the tiger.[(((triple4) -> rule7))] The mouse is red.[(((triple7) -> rule1))] The mouse sees the tiger.[(((triple2) -> rule2))] The tiger is nice.[(((triple10) -> rule4))] @2: The mouse chases the bear.[(((((triple7) -> rule1) triple8) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple8
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple9
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The bear is nice.
("bear" "is" "nice" "+")
((triple3) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((triple1) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple4) -> (rule7 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple7) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple10) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((((triple7) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2