The bear chases the tiger. The bear is blue. The bear is rough. The bear does not need the dog. The bear needs the mouse. The dog chases the mouse. The dog is young. The dog needs the tiger. The mouse eats the bear. The mouse eats the tiger. The mouse needs the dog. The mouse needs the tiger. The tiger does not eat the dog. The tiger eats the mouse. The tiger is blue. The tiger needs the mouse. If the mouse chases the bear and the mouse needs the tiger then the bear eats the tiger. If someone eats the dog then the dog eats the bear. If the tiger needs the mouse then the mouse eats the dog. If the dog eats the bear then the dog needs the bear. If someone needs the mouse then they need the tiger. If someone eats the bear and the bear is green then the bear does not eat the dog. If someone chases the tiger and they do not need the bear then the tiger is blue. If the tiger is kind and the tiger is not blue then the tiger does not chase the dog.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear does not need the dog.
("bear" "needs" "dog" "-")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If the mouse chases the bear and the mouse needs the tiger then the bear eats the tiger.
((("mouse" "chases" "bear" "+") ("mouse" "needs" "tiger" "+")) -> ("bear" "eats" "tiger" "+"))
If someone eats the dog then the dog eats the bear.
((("someone" "eats" "dog" "+")) -> ("dog" "eats" "bear" "+"))
If the tiger needs the mouse then the mouse eats the dog.
((("tiger" "needs" "mouse" "+")) -> ("mouse" "eats" "dog" "+"))
If the dog eats the bear then the dog needs the bear.
((("dog" "eats" "bear" "+")) -> ("dog" "needs" "bear" "+"))
If someone needs the mouse then they need the tiger.
((("someone" "needs" "mouse" "+")) -> ("someone" "needs" "tiger" "+"))
If someone eats the bear and the bear is green then the bear does not eat the dog.
((("someone" "eats" "bear" "+") ("bear" "is" "green" "+")) -> ("bear" "eats" "dog" "-"))
If someone chases the tiger and they do not need the bear then the tiger is blue.
((("someone" "chases" "tiger" "+") ("someone" "needs" "bear" "~")) -> ("tiger" "is" "blue" "+"))
If the tiger is kind and the tiger is not blue then the tiger does not chase the dog.
((("tiger" "is" "kind" "+") ("tiger" "is" "blue" "~")) -> ("tiger" "chases" "dog" "-"))
The dog needs the tiger.
True
1
proof
[(triple8)]
("dog" "needs" "tiger" "+")
triple8
The dog does not chase the mouse.
False
1
inv-proof
[(triple6)]
("dog" "chases" "mouse" "-")
triple6
The tiger needs the tiger.
True
2
proof
[(((triple16) -> rule5))]
("tiger" "needs" "tiger" "+")
((triple16) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The mouse does not eat the dog.
False
2
inv-proof
[(((triple16) -> rule3))]
("mouse" "eats" "dog" "-")
((triple16) -> (rule3 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The dog eats the bear.
True
3
proof
[(((((triple16) -> rule3)) -> rule2))]
("dog" "eats" "bear" "+")
((((triple16) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The dog does not eat the bear.
False
3
inv-proof
[(((((triple16) -> rule3)) -> rule2))]
("dog" "eats" "bear" "-")
((((triple16) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The dog needs the bear.
True
4
proof
[(((((((triple16) -> rule3)) -> rule2)) -> rule4))]
("dog" "needs" "bear" "+")
((((((triple16) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The dog does not need the bear.
False
4
inv-proof
[(((((((triple16) -> rule3)) -> rule2)) -> rule4))]
("dog" "needs" "bear" "-")
((((((triple16) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
The dog does not need the mouse.
Unknown
inv-random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The bear chases the tiger.[(triple1)] The bear does not need the dog.[(triple4)] The bear is blue.[(triple2)] The bear is rough.[(triple3)] The bear needs the mouse.[(triple5)] The dog chases the mouse.[(triple6)] The dog is young.[(triple7)] The dog needs the tiger.[(triple8)] The mouse eats the bear.[(triple9)] The mouse eats the tiger.[(triple10)] The mouse needs the dog.[(triple11)] The mouse needs the tiger.[(triple12)] The tiger does not eat the dog.[(triple13)] The tiger eats the mouse.[(triple14)] The tiger is blue.[(triple15)] The tiger needs the mouse.[(triple16)] @1: The bear needs the tiger.[(((triple5) -> rule5))] The mouse eats the dog.[(((triple16) -> rule3))] The tiger needs the tiger.[(((triple16) -> rule5))] @2: The dog eats the bear.[(((((triple16) -> rule3)) -> rule2))] @3: The dog needs the bear.[(((((((triple16) -> rule3)) -> rule2)) -> rule4))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear does not need the dog.
("bear" "needs" "dog" "-")
triple4
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple5
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple8
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple9
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple10
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple11
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple12
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
triple13
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple14
The tiger is blue.
("tiger" "is" "blue" "+")
triple15
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple16
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple5) -> (rule5 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple16) -> (rule3 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple16) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
((((triple16) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The dog needs the bear.
("dog" "needs" "bear" "+")
((((((triple16) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3