The cow is round. If something is nice then it is blue. If something is blue and nice then it is green. If the cow is round then the cow is nice. If the cow is not green and the cow is not blue then the cow is not kind. If something is nice then it is kind. If something is green and not blue then it is kind.
The cow is round.
("cow" "is" "round" "+")
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is blue and nice then it is green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If the cow is round then the cow is nice.
((("cow" "is" "round" "+")) -> ("cow" "is" "nice" "+"))
If the cow is not green and the cow is not blue then the cow is not kind.
((("cow" "is" "green" "~") ("cow" "is" "blue" "~")) -> ("cow" "is" "kind" "-"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is green and not blue then it is kind.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "+"))
The cow is round.
True
1
proof
[(triple1)]
("cow" "is" "round" "+")
triple1
The cow is not round.
False
1
inv-proof
[(triple1)]
("cow" "is" "round" "-")
triple1
The cow is nice.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("cow" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is green.
True
6
proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
("cow" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is not green.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
("cow" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
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 cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is round.[(triple1)] @1: The cow is nice.[(((triple1) -> rule3))] @2: The cow is blue.[(((((triple1) -> rule3)) -> rule1))] The cow is kind.[(((((triple1) -> rule3)) -> rule5))] @3: The cow is green.[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3