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