The cow is big. The cow visits the lion. The cow visits the mouse. The lion likes the squirrel. The mouse is kind. The mouse does not see the squirrel. The squirrel sees the cow. If someone likes the lion and the lion is rough then the lion likes the cow. If the squirrel visits the cow then the squirrel likes the cow. If someone likes the mouse then the mouse sees the squirrel. If someone visits the lion then the lion is big. If someone is rough then they do not like the squirrel. If someone is nice and big then they do not visit the cow. If someone is big then they are nice. If the squirrel sees the mouse and the squirrel is not green then the squirrel visits the lion.
The cow is big.
("cow" "is" "big" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If someone likes the lion and the lion is rough then the lion likes the cow.
((("someone" "likes" "lion" "+") ("lion" "is" "rough" "+")) -> ("lion" "likes" "cow" "+"))
If the squirrel visits the cow then the squirrel likes the cow.
((("squirrel" "visits" "cow" "+")) -> ("squirrel" "likes" "cow" "+"))
If someone likes the mouse then the mouse sees the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If someone visits the lion then the lion is big.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "big" "+"))
If someone is rough then they do not like the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "squirrel" "-"))
If someone is nice and big then they do not visit the cow.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "visits" "cow" "-"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If the squirrel sees the mouse and the squirrel is not green then the squirrel visits the lion.
((("squirrel" "sees" "mouse" "+") ("squirrel" "is" "green" "~")) -> ("squirrel" "visits" "lion" "+"))
The cow visits the lion.
True
1
proof
[(triple2)]
("cow" "visits" "lion" "+")
triple2
The squirrel does not see the cow.
False
1
inv-proof
[(triple7)]
("squirrel" "sees" "cow" "-")
triple7
The lion is big.
True
2
proof
[(((triple2) -> rule4))]
("lion" "is" "big" "+")
((triple2) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule7))]
("cow" "is" "nice" "-")
((triple1) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow does not visit the cow.
True
4
proof
[(((((triple1) -> rule7) triple1) -> rule6))]
("cow" "visits" "cow" "-")
((((triple1) -> (rule7 % int2)) triple1) -> (rule6 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The lion is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("lion" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not visit the cow.
True
6
proof
[(((((((triple2) -> rule4)) -> rule7) ((triple2) -> rule4)) -> rule6))]
("lion" "visits" "cow" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
The lion does not visit the cow.
("lion" "visits" "cow" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion visits the cow.
False
6
inv-proof
[(((((((triple2) -> rule4)) -> rule7) ((triple2) -> rule4)) -> rule6))]
("lion" "visits" "cow" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
The lion does not visit the cow.
("lion" "visits" "cow" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "nice" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "nice" "+")
The squirrel does not visit the lion.
Unknown
inv-rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "lion" "-")
The squirrel likes the cow.
Unknown
rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "cow" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow sees the squirrel.
Unknown
random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "+")
The lion does not like the mouse.
Unknown
inv-random
[@0: The lion likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "mouse" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cow is big.[(triple1)] The cow visits the lion.[(triple2)] The cow visits the mouse.[(triple3)] The lion likes the squirrel.[(triple4)] The mouse does not see the squirrel.[(triple6)] The mouse is kind.[(triple5)] The squirrel sees the cow.[(triple7)] @1: The cow is nice.[(((triple1) -> rule7))] The lion is big.[(((triple2) -> rule4))] @2: The cow does not visit the cow.[(((((triple1) -> rule7) triple1) -> rule6))] The lion is nice.[(((((triple2) -> rule4)) -> rule7))] @3: The lion does not visit the cow.[(((((((triple2) -> rule4)) -> rule7) ((triple2) -> rule4)) -> rule6))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow visits the lion.
("cow" "visits" "lion" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple4
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((triple2) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cow does not visit the cow.
("cow" "visits" "cow" "-")
((((triple1) -> (rule7 % int2)) triple1) -> (rule6 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not visit the cow.
("lion" "visits" "cow" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
The lion does not visit the cow.
("lion" "visits" "cow" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3