The cow chases the squirrel. The cow is cold. The cow is green. The cow sees the squirrel. The cow does not visit the squirrel. The squirrel does not chase the cow. The squirrel is green. The squirrel is round. The squirrel does not see the cow. The squirrel visits the cow. If someone chases the cow and the cow visits the squirrel then the squirrel chases the cow. If someone sees the squirrel then they do not visit the squirrel. If the cow is round and the cow does not chase the squirrel then the squirrel sees the cow. If the cow is round then the cow is green. If someone is cold and they see the cow then the cow sees the squirrel. If someone sees the squirrel then they visit the cow. If someone visits the cow then they are kind. If someone is kind then they see the squirrel.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone chases the cow and the cow visits the squirrel then the squirrel chases the cow.
((("someone" "chases" "cow" "+") ("cow" "visits" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
If someone sees the squirrel then they do not visit the squirrel.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "squirrel" "-"))
If the cow is round and the cow does not chase the squirrel then the squirrel sees the cow.
((("cow" "is" "round" "+") ("cow" "chases" "squirrel" "~")) -> ("squirrel" "sees" "cow" "+"))
If the cow is round then the cow is green.
((("cow" "is" "round" "+")) -> ("cow" "is" "green" "+"))
If someone is cold and they see the cow then the cow sees the squirrel.
((("someone" "is" "cold" "+") ("someone" "sees" "cow" "+")) -> ("cow" "sees" "squirrel" "+"))
If someone sees the squirrel then they visit the cow.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cow then they are kind.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they see the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "squirrel" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The squirrel does not visit the cow.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "cow" "-")
triple10
The squirrel is kind.
True
2
proof
[(((triple10) -> rule7))]
("squirrel" "is" "kind" "+")
((triple10) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple4) -> rule6))]
("cow" "visits" "cow" "-")
((triple4) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is kind.
True
3
proof
[(((((triple4) -> rule6)) -> rule7))]
("cow" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((((triple10) -> rule7)) -> rule8))]
("squirrel" "sees" "squirrel" "-")
((((triple10) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The cow chases the squirrel.[(triple1)] The cow does not visit the squirrel.[(triple5 OR ((triple4) -> rule2))] The cow is cold.[(triple2)] The cow is green.[(triple3)] The cow sees the squirrel.[(triple4)] The squirrel does not chase the cow.[(triple6)] The squirrel does not see the cow.[(triple9)] The squirrel is green.[(triple7)] The squirrel is round.[(triple8)] The squirrel visits the cow.[(triple10)] @1: The cow visits the cow.[(((triple4) -> rule6))] The squirrel is kind.[(((triple10) -> rule7))] @2: The cow is kind.[(((((triple4) -> rule6)) -> rule7))] The squirrel sees the squirrel.[(((((triple10) -> rule7)) -> rule8))] @3: The squirrel does not visit the squirrel.[(((((((triple10) -> rule7)) -> rule8)) -> rule2))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
triple5
((triple4) -> (rule2 % int1))
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple4
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
triple6
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
triple9
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel is round.
("squirrel" "is" "round" "+")
triple8
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple10
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple4) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple10) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple10) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
((((((triple10) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3