The cat is green. The cow is not kind. The cow is rough. The mouse chases the cow. The mouse is cold. The mouse is green. The mouse is kind. The squirrel is green. The squirrel is kind. The squirrel does not like the mouse. If something is big then it chases the mouse. If something chases the cat and the cat chases the cow then the cow chases the cat. Kind things are not rough. If something needs the squirrel and it needs the cat then the cat does not need the cow. If something is cold and it does not need the squirrel then it does not chase the cat. If something is rough and it does not like the cow then the cow likes the cat. If something chases the cow and it is not rough then the cow likes the cat. If something likes the cat then the cat does not like the squirrel.
The cat is green.
("cat" "is" "green" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is rough.
("cow" "is" "rough" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the cat and the cat chases the cow then the cow chases the cat.
((("something" "chases" "cat" "+") ("cat" "chases" "cow" "+")) -> ("cow" "chases" "cat" "+"))
Kind things are not rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "-"))
If something needs the squirrel and it needs the cat then the cat does not need the cow.
((("something" "needs" "squirrel" "+") ("something" "needs" "cat" "+")) -> ("cat" "needs" "cow" "-"))
If something is cold and it does not need the squirrel then it does not chase the cat.
((("something" "is" "cold" "+") ("something" "needs" "squirrel" "~")) -> ("something" "chases" "cat" "-"))
If something is rough and it does not like the cow then the cow likes the cat.
((("something" "is" "rough" "+") ("something" "likes" "cow" "~")) -> ("cow" "likes" "cat" "+"))
If something chases the cow and it is not rough then the cow likes the cat.
((("something" "chases" "cow" "+") ("something" "is" "rough" "~")) -> ("cow" "likes" "cat" "+"))
If something likes the cat then the cat does not like the squirrel.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "squirrel" "-"))
The mouse chases the cow.
True
1
proof
[(triple4)]
("mouse" "chases" "cow" "+")
triple4
The cow is not rough.
False
1
inv-proof
[(triple3)]
("cow" "is" "rough" "-")
triple3
The squirrel does not chase the mouse.
Unknown
inv-rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "mouse" "-")
The cat likes the mouse.
Unknown
random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "+")
@0: The cat is green.[(triple1)] The cow is not kind.[(triple2)] The cow is rough.[(triple3)] The mouse chases the cow.[(triple4)] The mouse is cold.[(triple5)] The mouse is green.[(triple6)] The mouse is kind.[(triple7)] The squirrel does not like the mouse.[(triple10)] The squirrel is green.[(triple8)] The squirrel is kind.[(triple9)] @1: The mouse is not rough.[(((triple7) -> rule3))] The squirrel is not rough.[(((triple9) -> rule3))] @2: The cow likes the cat.[(((triple4 ((triple7) -> rule3)) -> rule7))] @3: The cat does not like the squirrel.[(((((triple4 ((triple7) -> rule3)) -> rule7)) -> rule8))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cow is not kind.
("cow" "is" "kind" "-")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple4
The mouse is cold.
("mouse" "is" "cold" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The mouse is not rough.
("mouse" "is" "rough" "-")
((triple7) -> (rule3 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The squirrel is not rough.
("squirrel" "is" "rough" "-")
((triple9) -> (rule3 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
((triple4 ((triple7) -> (rule3 % int2))) -> (rule7 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The mouse is not rough.
("mouse" "is" "rough" "-")
int2
The cat does not like the squirrel.
("cat" "likes" "squirrel" "-")
((((triple4 ((triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat does not like the squirrel.
("cat" "likes" "squirrel" "-")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The mouse is not rough.
("mouse" "is" "rough" "-")
int3