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