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