The cow is blue. The cow is nice. The cow is young. The cow does not like the mouse. The cow needs the squirrel. The cow sees the mouse. The cow sees the squirrel. The mouse is blue. The mouse is cold. The mouse is young. The mouse sees the cow. The mouse sees the squirrel. The squirrel is kind. The squirrel is nice. The squirrel does not see the cow. The squirrel sees the mouse. If someone likes the cow and they like the mouse then the mouse is not cold. If someone is cold and they do not like the cow then they see the mouse. If someone sees the squirrel then the squirrel is not young. If the cow needs the squirrel and the squirrel needs the mouse then the cow likes the mouse. Nice people are kind. If someone needs the mouse then the mouse needs the cow. If someone needs the squirrel and they see the cow then the cow needs the mouse. If someone is blue then they need the squirrel.
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone likes the cow and they like the mouse then the mouse is not cold.
((("someone" "likes" "cow" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "-"))
If someone is cold and they do not like the cow then they see the mouse.
((("someone" "is" "cold" "+") ("someone" "likes" "cow" "~")) -> ("someone" "sees" "mouse" "+"))
If someone sees the squirrel then the squirrel is not young.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "is" "young" "-"))
If the cow needs the squirrel and the squirrel needs the mouse then the cow likes the mouse.
((("cow" "needs" "squirrel" "+") ("squirrel" "needs" "mouse" "+")) -> ("cow" "likes" "mouse" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the mouse then the mouse needs the cow.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "cow" "+"))
If someone needs the squirrel and they see the cow then the cow needs the mouse.
((("someone" "needs" "squirrel" "+") ("someone" "sees" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
If someone is blue then they need the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
The mouse sees the cow.
True
1
proof
[(triple11)]
("mouse" "sees" "cow" "+")
triple11
The cow does not see the squirrel.
False
1
inv-proof
[(triple7)]
("cow" "sees" "squirrel" "-")
triple7
The squirrel is not young.
True
2
proof
[(((triple12) -> rule3) OR ((triple7) -> rule3))]
("squirrel" "is" "young" "-")
((triple12) -> (rule3 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
((triple7) -> (rule3 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The mouse does not need the squirrel.
False
2
inv-proof
[(((triple8) -> rule8))]
("mouse" "needs" "squirrel" "-")
((triple8) -> (rule8 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The cow needs the mouse.
True
4
proof
[(((((triple8) -> rule8) triple11) -> rule7))]
("cow" "needs" "mouse" "+")
((((triple8) -> (rule8 % int2)) triple11) -> (rule7 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The cow does not need the mouse.
False
4
inv-proof
[(((((triple8) -> rule8) triple11) -> rule7))]
("cow" "needs" "mouse" "-")
((((triple8) -> (rule8 % int2)) triple11) -> (rule7 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse needs the cow.
True
5
proof
[(((((((triple8) -> rule8) triple11) -> rule7)) -> rule6))]
("mouse" "needs" "cow" "+")
((((((triple8) -> (rule8 % int3)) triple11) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The mouse does not need the cow.
False
5
inv-proof
[(((((((triple8) -> rule8) triple11) -> rule7)) -> rule6))]
("mouse" "needs" "cow" "-")
((((((triple8) -> (rule8 % int3)) triple11) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "kind" "-")
The squirrel likes the cow.
Unknown
random
[@0: The squirrel likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cow" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "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 cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow does not like the mouse.[(triple4)] The cow is blue.[(triple1)] The cow is nice.[(triple2)] The cow is young.[(triple3)] The cow needs the squirrel.[(triple5 OR ((triple1) -> rule8))] The cow sees the mouse.[(triple6)] The cow sees the squirrel.[(triple7)] The mouse is blue.[(triple8)] The mouse is cold.[(triple9)] The mouse is young.[(triple10)] The mouse sees the cow.[(triple11)] The mouse sees the squirrel.[(triple12)] The squirrel does not see the cow.[(triple15)] The squirrel is kind.[(triple13 OR ((triple14) -> rule5))] The squirrel is nice.[(triple14)] The squirrel sees the mouse.[(triple16)] @1: The cow is kind.[(((triple2) -> rule5))] The mouse needs the squirrel.[(((triple8) -> rule8))] The squirrel is not young.[(((triple12) -> rule3) OR ((triple7) -> rule3))] @2: The cow needs the mouse.[(((((triple8) -> rule8) triple11) -> rule7))] @3: The mouse needs the cow.[(((((((triple8) -> rule8) triple11) -> rule7)) -> rule6))]
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple5
((triple1) -> (rule8 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple12
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
triple15
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple13
((triple14) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple14
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple16
The cow is kind.
("cow" "is" "kind" "+")
((triple2) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple8) -> (rule8 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel is not young.
("squirrel" "is" "young" "-")
((triple12) -> (rule3 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
((triple7) -> (rule3 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((((triple8) -> (rule8 % int2)) triple11) -> (rule7 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((((((triple8) -> (rule8 % int3)) triple11) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3