The cow is round. If the cow is blue then the cow is cold. All cold, blue people are rough. Round people are blue.
The cow is round.
("cow" "is" "round" "+")
If the cow is blue then the cow is cold.
((("cow" "is" "blue" "+")) -> ("cow" "is" "cold" "+"))
All cold, blue people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
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 blue.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is rough.
True
6
proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
("cow" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is not rough.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
("cow" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
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 eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow is round.[(triple1)] @1: The cow is blue.[(((triple1) -> rule3))] @2: The cow is cold.[(((((triple1) -> rule3)) -> rule1))] @3: The cow is rough.[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3