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