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