The cow is blue. If something is blue then it is kind. If something is kind and blue then it is rough. If the cow is kind and the cow is cold then the cow is rough. Rough things are cold. If the cow is cold and the cow is kind then the cow is blue. If something is kind then it is blue.
The cow is blue.
("cow" "is" "blue" "+")
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is kind and blue then it is rough.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If the cow is kind and the cow is cold then the cow is rough.
((("cow" "is" "kind" "+") ("cow" "is" "cold" "+")) -> ("cow" "is" "rough" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If the cow is cold and the cow is kind then the cow is blue.
((("cow" "is" "cold" "+") ("cow" "is" "kind" "+")) -> ("cow" "is" "blue" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The cow is kind.
True
2
proof
[(((triple1) -> rule1))]
("cow" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is rough.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("cow" "is" "rough" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is not rough.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("cow" "is" "rough" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is cold.
True
5
proof
[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule4))]
("cow" "is" "cold" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow is not cold.
False
5
inv-proof
[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule4))]
("cow" "is" "cold" "-")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is blue.[(triple1)] @1: The cow is kind.[(((triple1) -> rule1))] @2: The cow is rough.[(((((triple1) -> rule1) triple1) -> rule2))] @3: The cow is cold.[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule4))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3