The cow is nice. All nice, red people are kind. Young people are nice. If someone is young then they are red. All nice people are kind. If someone is green and kind then they are nice. All green, nice people are young. If the cow is kind then the cow is green. All red people are young.
The cow is nice.
("cow" "is" "nice" "+")
All nice, red people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and kind then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All green, nice people are young.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If the cow is kind then the cow is green.
((("cow" "is" "kind" "+")) -> ("cow" "is" "green" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
The cow is nice.
True
1
proof
[(triple1)]
("cow" "is" "nice" "+")
triple1
The cow is not nice.
False
1
inv-proof
[(triple1)]
("cow" "is" "nice" "-")
triple1
The cow is kind.
True
2
proof
[(((triple1) -> rule4))]
("cow" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "is" "kind" "-")
((triple1) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is green.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("cow" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is not green.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("cow" "is" "green" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is young.
True
5
proof
[(((((((triple1) -> rule4)) -> rule7) triple1) -> rule6))]
("cow" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow is not young.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule7) triple1) -> rule6))]
("cow" "is" "young" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is nice.[(triple1)] @1: The cow is kind.[(((triple1) -> rule4))] @2: The cow is green.[(((((triple1) -> rule4)) -> rule7))] @3: The cow is young.[(((((((triple1) -> rule4)) -> rule7) triple1) -> rule6))] @4: The cow is red.[(((((((((triple1) -> rule4)) -> rule7) triple1) -> rule6)) -> rule3))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is young.
("cow" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow is red.
("cow" "is" "red" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4