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