The cow is red. Cold people are round. All nice people are round. If someone is round and rough then they are nice. If someone is red then they are round. If the cow is rough and the cow is cold then the cow is nice. If the cow is round then the cow is rough.
The cow is red.
("cow" "is" "red" "+")
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is round and rough then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If the cow is rough and the cow is cold then the cow is nice.
((("cow" "is" "rough" "+") ("cow" "is" "cold" "+")) -> ("cow" "is" "nice" "+"))
If the cow is round then the cow is rough.
((("cow" "is" "round" "+")) -> ("cow" "is" "rough" "+"))
The cow is red.
True
1
proof
[(triple1)]
("cow" "is" "red" "+")
triple1
The cow is not red.
False
1
inv-proof
[(triple1)]
("cow" "is" "red" "-")
triple1
The cow is round.
True
2
proof
[(((triple1) -> rule4))]
("cow" "is" "round" "+")
((triple1) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "is" "round" "-")
((triple1) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is rough.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("cow" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is not rough.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("cow" "is" "rough" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is nice.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule6)) -> rule3))]
("cow" "is" "nice" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow is not nice.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule6)) -> rule3))]
("cow" "is" "nice" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is round.
("cow" "is" "round" "+")
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" "+")
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 is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow is red.[(triple1)] @1: The cow is round.[(((triple1) -> rule4))] @2: The cow is rough.[(((((triple1) -> rule4)) -> rule6))] @3: The cow is nice.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule6)) -> rule3))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
((triple1) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3