The cow is cold. All nice, cold things are big. If the cow is nice then the cow is blue. If something is rough then it is nice. All blue things are rough. Cold things are rough. All rough, nice things are cold.
The cow is cold.
("cow" "is" "cold" "+")
All nice, cold things are big.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If the cow is nice then the cow is blue.
((("cow" "is" "nice" "+")) -> ("cow" "is" "blue" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All rough, nice things are cold.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The cow is not cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The cow is rough.
True
2
proof
[(((triple1) -> rule5))]
("cow" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("cow" "is" "rough" "-")
((triple1) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("cow" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is not nice.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("cow" "is" "nice" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is big.
True
5
proof
[(((((((triple1) -> rule5)) -> rule3) triple1) -> rule1))]
("cow" "is" "big" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is not big.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule3) triple1) -> rule1))]
("cow" "is" "big" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is 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 likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow is cold.[(triple1)] @1: The cow is rough.[(((triple1) -> rule5))] @2: The cow is nice.[(((((triple1) -> rule5)) -> rule3))] @3: The cow is big.[(((((((triple1) -> rule5)) -> rule3) triple1) -> rule1))] The cow is blue.[(((((((triple1) -> rule5)) -> rule3)) -> rule2))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3