The cow is red. If the cow is nice and the cow is rough then the cow is blue. All nice, red people are rough. If someone is red then they are nice.
The cow is red.
("cow" "is" "red" "+")
If the cow is nice and the cow is rough then the cow is blue.
((("cow" "is" "nice" "+") ("cow" "is" "rough" "+")) -> ("cow" "is" "blue" "+"))
All nice, red people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
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 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 rough.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule2))]
("cow" "is" "rough" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is not rough.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule2))]
("cow" "is" "rough" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is blue.
True
7
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3) triple1) -> rule2)) -> rule1))]
("cow" "is" "blue" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is not blue.
False
7
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3) triple1) -> rule2)) -> rule1))]
("cow" "is" "blue" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
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 is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "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 red.[(triple1)] @1: The cow is nice.[(((triple1) -> rule3))] @2: The cow is rough.[(((((triple1) -> rule3) triple1) -> rule2))] @3: The cow is blue.[(((((triple1) -> rule3) ((((triple1) -> rule3) triple1) -> rule2)) -> rule1))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3