The cow is rough. The mouse is red. The squirrel likes the mouse. If the mouse sees the cow and the cow likes the squirrel then the cow is green. If someone is rough and they chase the squirrel then they do not chase the cow. If someone likes the mouse then they are rough. If someone sees the cow and they are not cold then they are rough. If someone likes the cow then the cow chases the squirrel. If someone is rough then they chase the squirrel.
The cow is rough.
("cow" "is" "rough" "+")
The mouse is red.
("mouse" "is" "red" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If the mouse sees the cow and the cow likes the squirrel then the cow is green.
((("mouse" "sees" "cow" "+") ("cow" "likes" "squirrel" "+")) -> ("cow" "is" "green" "+"))
If someone is rough and they chase the squirrel then they do not chase the cow.
((("someone" "is" "rough" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "cow" "-"))
If someone likes the mouse then they are rough.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the cow and they are not cold then they are rough.
((("someone" "sees" "cow" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
If someone likes the cow then the cow chases the squirrel.
((("someone" "likes" "cow" "+")) -> ("cow" "chases" "squirrel" "+"))
If someone is rough then they chase the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "squirrel" "+"))
The cow is rough.
True
1
proof
[(triple1)]
("cow" "is" "rough" "+")
triple1
The cow is not rough.
False
1
inv-proof
[(triple1)]
("cow" "is" "rough" "-")
triple1
The cow chases the squirrel.
True
2
proof
[(((triple1) -> rule6))]
("cow" "chases" "squirrel" "+")
((triple1) -> (rule6 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "is" "rough" "-")
((triple3) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("squirrel" "chases" "squirrel" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The cow chases the cow.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("cow" "chases" "cow" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The squirrel does not chase the cow.
True
6
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule6)) -> rule2))]
("squirrel" "chases" "cow" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel chases the cow.
False
6
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule6)) -> rule2))]
("squirrel" "chases" "cow" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "green" "-")
The mouse chases the squirrel.
Unknown
rconc
[@2: The mouse chases the squirrel.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("mouse" "chases" "squirrel" "+")
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "rough" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
@0: The cow is rough.[(triple1)] The mouse is red.[(triple2)] The squirrel likes the mouse.[(triple3)] @1: The cow chases the squirrel.[(((triple1) -> rule6))] The squirrel is rough.[(((triple3) -> rule3))] @2: The cow does not chase the cow.[(((triple1 ((triple1) -> rule6)) -> rule2))] The squirrel chases the squirrel.[(((((triple3) -> rule3)) -> rule6))] @3: The squirrel does not chase the cow.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule6)) -> rule2))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple3
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((triple1) -> (rule6 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple3) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The cow does not chase the cow.
("cow" "chases" "cow" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3