The bear is not green. The bear is young. The bear sees the tiger. The dog needs the mouse. The mouse is big. The mouse needs the bear. The mouse needs the dog. The mouse needs the tiger. The tiger is not big. The tiger is not young. The tiger needs the dog. The tiger sees the mouse. If someone needs the dog then they see the mouse. If the tiger needs the dog then the dog is big. If someone eats the dog then they eat the tiger. If someone is rough and they need the mouse then they eat the tiger. If someone sees the mouse then they do not eat the dog. If someone is big then they eat the bear. If someone eats the bear then they need the dog.
The bear is not green.
("bear" "is" "green" "-")
The bear is young.
("bear" "is" "young" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone needs the dog then they see the mouse.
((("someone" "needs" "dog" "+")) -> ("someone" "sees" "mouse" "+"))
If the tiger needs the dog then the dog is big.
((("tiger" "needs" "dog" "+")) -> ("dog" "is" "big" "+"))
If someone eats the dog then they eat the tiger.
((("someone" "eats" "dog" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is rough and they need the mouse then they eat the tiger.
((("someone" "is" "rough" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "eats" "tiger" "+"))
If someone sees the mouse then they do not eat the dog.
((("someone" "sees" "mouse" "+")) -> ("someone" "eats" "dog" "-"))
If someone is big then they eat the bear.
((("someone" "is" "big" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the bear then they need the dog.
((("someone" "eats" "bear" "+")) -> ("someone" "needs" "dog" "+"))
The dog needs the mouse.
True
1
proof
[(triple4)]
("dog" "needs" "mouse" "+")
triple4
The bear is green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "+")
triple1
The dog is big.
True
2
proof
[(((triple11) -> rule2))]
("dog" "is" "big" "+")
((triple11) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The mouse does not eat the bear.
False
2
inv-proof
[(((triple5) -> rule6))]
("mouse" "eats" "bear" "-")
((triple5) -> (rule6 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not eat the dog.
True
3
proof
[(((((triple7) -> rule1)) -> rule5) OR ((((((((triple5) -> rule6)) -> rule7)) -> rule1)) -> rule5))]
("mouse" "eats" "dog" "-")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int4
The mouse eats the dog.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule5) OR ((((((((triple5) -> rule6)) -> rule7)) -> rule1)) -> rule5))]
("mouse" "eats" "dog" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int4
The dog needs the dog.
True
4
proof
[(((((((triple11) -> rule2)) -> rule6)) -> rule7))]
("dog" "needs" "dog" "+")
((((((triple11) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((((triple11) -> rule2)) -> rule6)) -> rule7))]
("dog" "needs" "dog" "-")
((((((triple11) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog sees the mouse.
True
5
proof
[(((((((((triple11) -> rule2)) -> rule6)) -> rule7)) -> rule1))]
("dog" "sees" "mouse" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
int3
The dog is big.
("dog" "is" "big" "+")
int4
The dog does not see the mouse.
False
5
inv-proof
[(((((((((triple11) -> rule2)) -> rule6)) -> rule7)) -> rule1))]
("dog" "sees" "mouse" "-")
((((((((triple11) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
int3
The dog is big.
("dog" "is" "big" "+")
int4
The dog does not eat the dog.
True
6
proof
[(((((((((((triple11) -> rule2)) -> rule6)) -> rule7)) -> rule1)) -> rule5))]
("dog" "eats" "dog" "-")
((((((((((triple11) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The dog eats the bear.
("dog" "eats" "bear" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5
The dog eats the dog.
False
6
inv-proof
[(((((((((((triple11) -> rule2)) -> rule6)) -> rule7)) -> rule1)) -> rule5))]
("dog" "eats" "dog" "+")
((((((((((triple11) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The dog eats the bear.
("dog" "eats" "bear" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "bear" "-")
The dog eats the tiger.
Unknown
rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "tiger" "+")
The tiger does not eat the bear.
Unknown
inv-rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "bear" "-")
The bear needs the dog.
Unknown
rconc
[@2: The bear needs the dog.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("bear" "needs" "dog" "+")
The mouse does not eat the tiger.
Unknown
inv-rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "tiger" "-")
The bear eats the tiger.
Unknown
rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "tiger" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
The tiger does not need the bear.
Unknown
inv-random
[@0: The tiger needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bear" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The bear is not green.[(triple1)] The bear is young.[(triple2)] The bear sees the tiger.[(triple3)] The dog needs the mouse.[(triple4)] The mouse is big.[(triple5)] The mouse needs the bear.[(triple6)] The mouse needs the dog.[(triple7 OR ((((triple5) -> rule6)) -> rule7))] The mouse needs the tiger.[(triple8)] The tiger is not big.[(triple9)] The tiger is not young.[(triple10)] The tiger needs the dog.[(triple11)] The tiger sees the mouse.[(triple12 OR ((triple11) -> rule1))] @1: The dog is big.[(((triple11) -> rule2))] The mouse eats the bear.[(((triple5) -> rule6))] The mouse sees the mouse.[(((triple7) -> rule1) OR ((((((triple5) -> rule6)) -> rule7)) -> rule1))] The tiger does not eat the dog.[(((triple12) -> rule5) OR ((((triple11) -> rule1)) -> rule5))] @2: The dog eats the bear.[(((((triple11) -> rule2)) -> rule6))] The mouse does not eat the dog.[(((((triple7) -> rule1)) -> rule5) OR ((((((((triple5) -> rule6)) -> rule7)) -> rule1)) -> rule5))] @3: The dog needs the dog.[(((((((triple11) -> rule2)) -> rule6)) -> rule7))] @4: The dog sees the mouse.[(((((((((triple11) -> rule2)) -> rule6)) -> rule7)) -> rule1))] @5: The dog does not eat the dog.[(((((((((((triple11) -> rule2)) -> rule6)) -> rule7)) -> rule1)) -> rule5))]
The bear is not green.
("bear" "is" "green" "-")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple6
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple7
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple8
The tiger is not big.
("tiger" "is" "big" "-")
triple9
The tiger is not young.
("tiger" "is" "young" "-")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
((triple11) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((triple11) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple5) -> (rule6 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple7) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
((((((triple5) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
((triple12) -> (rule5 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
((((triple11) -> (rule1 % int2))) -> (rule5 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse does not eat the dog.
("mouse" "eats" "dog" "-")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int4
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple11) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
int3
The dog is big.
("dog" "is" "big" "+")
int4
The dog does not eat the dog.
("dog" "eats" "dog" "-")
((((((((((triple11) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The dog eats the bear.
("dog" "eats" "bear" "+")
int4
The dog is big.
("dog" "is" "big" "+")
int5