The cow is kind. If the cow is kind then the cow is not rough. If something is rough then it is kind. All rough, blue things are green. If something is green and not rough then it is blue. If something is green and not rough then it is blue. All kind things are round. If something is green and blue then it is round. If the cow is not rough then the cow is green.
The cow is kind.
("cow" "is" "kind" "+")
If the cow is kind then the cow is not rough.
((("cow" "is" "kind" "+")) -> ("cow" "is" "rough" "-"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All rough, blue things are green.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is green and not rough then it is blue.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "is" "blue" "+"))
If something is green and not rough then it is blue.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "is" "blue" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is green and blue then it is round.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If the cow is not rough then the cow is green.
((("cow" "is" "rough" "~")) -> ("cow" "is" "green" "+"))
The cow is kind.
True
1
proof
[(triple1)]
("cow" "is" "kind" "+")
triple1
The cow is not kind.
False
1
inv-proof
[(triple1)]
("cow" "is" "kind" "-")
triple1
The cow is not rough.
True
2
proof
[(((triple1) -> rule1))]
("cow" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The cow is not rough.
("cow" "is" "rough" "-")
int1
The cow is rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The cow is not rough.
("cow" "is" "rough" "-")
int1
The cow is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("cow" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not rough.
("cow" "is" "rough" "-")
int2
The cow is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("cow" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not rough.
("cow" "is" "rough" "-")
int2
The cow is blue.
True
6
proof
[(((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule5))]
("cow" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not rough.
("cow" "is" "rough" "-")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not rough.
("cow" "is" "rough" "-")
int3
The cow is not blue.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule5))]
("cow" "is" "blue" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not rough.
("cow" "is" "rough" "-")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not rough.
("cow" "is" "rough" "-")
int3
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is kind.[(triple1)] @1: The cow is not rough.[(((triple1) -> rule1))] The cow is round.[(((triple1) -> rule6) OR ((((((triple1) -> rule1)) -> rule8) ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule4)) -> rule7) OR ((((((triple1) -> rule1)) -> rule8) ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule5)) -> rule7))] @2: The cow is green.[(((((triple1) -> rule1)) -> rule8))] @3: The cow is blue.[(((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule5))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is not rough.
("cow" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The cow is not rough.
("cow" "is" "rough" "-")
int1
The cow is round.
("cow" "is" "round" "+")
((triple1) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((triple1) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is not rough.
("cow" "is" "rough" "-")
int4
((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((triple1) -> (rule1 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is not rough.
("cow" "is" "rough" "-")
int4
The cow is green.
("cow" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not rough.
("cow" "is" "rough" "-")
int2
The cow is blue.
("cow" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not rough.
("cow" "is" "rough" "-")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not rough.
("cow" "is" "rough" "-")
int3