The dog is big. The dog is kind. The dog sees the squirrel. The mouse eats the dog. The mouse is big. The mouse is kind. The mouse is rough. The mouse sees the squirrel. The squirrel eats the dog. The squirrel eats the mouse. The squirrel is big. The squirrel is nice. The squirrel needs the dog. The squirrel needs the mouse. The squirrel does not see the dog. The squirrel does not see the mouse. If the dog eats the squirrel then the dog is rough. If something needs the squirrel then it needs the dog. If something eats the dog and it eats the mouse then the mouse needs the squirrel. If something needs the mouse and it does not see the mouse then the mouse needs the squirrel. If something is kind and it needs the dog then the dog does not eat the mouse. If something is nice then it eats the mouse. If the mouse needs the dog then the mouse is rough. If the squirrel is blue and the squirrel is not nice then the squirrel sees the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel does not see the dog.
("squirrel" "sees" "dog" "-")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
If the dog eats the squirrel then the dog is rough.
((("dog" "eats" "squirrel" "+")) -> ("dog" "is" "rough" "+"))
If something needs the squirrel then it needs the dog.
((("something" "needs" "squirrel" "+")) -> ("something" "needs" "dog" "+"))
If something eats the dog and it eats the mouse then the mouse needs the squirrel.
((("something" "eats" "dog" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something needs the mouse and it does not see the mouse then the mouse needs the squirrel.
((("something" "needs" "mouse" "+") ("something" "sees" "mouse" "~")) -> ("mouse" "needs" "squirrel" "+"))
If something is kind and it needs the dog then the dog does not eat the mouse.
((("something" "is" "kind" "+") ("something" "needs" "dog" "+")) -> ("dog" "eats" "mouse" "-"))
If something is nice then it eats the mouse.
((("something" "is" "nice" "+")) -> ("something" "eats" "mouse" "+"))
If the mouse needs the dog then the mouse is rough.
((("mouse" "needs" "dog" "+")) -> ("mouse" "is" "rough" "+"))
If the squirrel is blue and the squirrel is not nice then the squirrel sees the dog.
((("squirrel" "is" "blue" "+") ("squirrel" "is" "nice" "~")) -> ("squirrel" "sees" "dog" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple10 OR ((triple12) -> rule6))]
("squirrel" "eats" "mouse" "+")
triple10
((triple12) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel sees the mouse.
False
1
inv-proof
[(triple16)]
("squirrel" "sees" "mouse" "+")
triple16
The mouse needs the squirrel.
True
3
proof
[(((triple14 triple16) -> rule4) OR ((triple9 triple10) -> rule3) OR ((triple9 ((triple12) -> rule6)) -> rule3))]
("mouse" "needs" "squirrel" "+")
((triple14 triple16) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple9 triple10) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple9 ((triple12) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse does not need the squirrel.
False
3
inv-proof
[(((triple14 triple16) -> rule4) OR ((triple9 triple10) -> rule3) OR ((triple9 ((triple12) -> rule6)) -> rule3))]
("mouse" "needs" "squirrel" "-")
((triple14 triple16) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple9 triple10) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple9 ((triple12) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse needs the dog.
True
4
proof
[(((((triple14 triple16) -> rule4)) -> rule2) OR ((((triple9 triple10) -> rule3)) -> rule2) OR ((((triple9 ((triple12) -> rule6)) -> rule3)) -> rule2))]
("mouse" "needs" "dog" "+")
((((triple14 triple16) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple9 triple10) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple9 ((triple12) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The mouse does not need the dog.
False
4
inv-proof
[(((((triple14 triple16) -> rule4)) -> rule2) OR ((((triple9 triple10) -> rule3)) -> rule2) OR ((((triple9 ((triple12) -> rule6)) -> rule3)) -> rule2))]
("mouse" "needs" "dog" "-")
((((triple14 triple16) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple9 triple10) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple9 ((triple12) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "rough" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "dog" "+")
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The dog is big.[(triple1)] The dog is kind.[(triple2)] The dog sees the squirrel.[(triple3)] The mouse eats the dog.[(triple4)] The mouse is big.[(triple5)] The mouse is kind.[(triple6)] The mouse is rough.[(triple7 OR ((((((triple14 triple16) -> rule4)) -> rule2)) -> rule7) OR ((((((triple9 triple10) -> rule3)) -> rule2)) -> rule7) OR ((((((triple9 ((triple12) -> rule6)) -> rule3)) -> rule2)) -> rule7))] The mouse sees the squirrel.[(triple8)] The squirrel does not see the dog.[(triple15)] The squirrel does not see the mouse.[(triple16)] The squirrel eats the dog.[(triple9)] The squirrel eats the mouse.[(triple10 OR ((triple12) -> rule6))] The squirrel is big.[(triple11)] The squirrel is nice.[(triple12)] The squirrel needs the dog.[(triple13)] The squirrel needs the mouse.[(triple14)] @1: The mouse needs the squirrel.[(((triple14 triple16) -> rule4) OR ((triple9 triple10) -> rule3) OR ((triple9 ((triple12) -> rule6)) -> rule3))] @2: The mouse needs the dog.[(((((triple14 triple16) -> rule4)) -> rule2) OR ((((triple9 triple10) -> rule3)) -> rule2) OR ((((triple9 ((triple12) -> rule6)) -> rule3)) -> rule2))] @3: The dog does not eat the mouse.[(((triple6 ((((triple14 triple16) -> rule4)) -> rule2)) -> rule5) OR ((triple6 ((((triple9 triple10) -> rule3)) -> rule2)) -> rule5) OR ((triple6 ((((triple9 ((triple12) -> rule6)) -> rule3)) -> rule2)) -> rule5))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
((((((triple14 triple16) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((((((triple9 triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((((((triple9 ((triple12) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The squirrel does not see the dog.
("squirrel" "sees" "dog" "-")
triple15
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple16
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple9
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple10
((triple12) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
triple11
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple12
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple13
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple14
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple14 triple16) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple9 triple10) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple9 ((triple12) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((triple14 triple16) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple9 triple10) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple9 ((triple12) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
((triple6 ((((triple14 triple16) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((triple6 ((((triple9 triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((triple6 ((((triple9 ((triple12) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int4