The cow is blue. The cow is red. The cow is rough. If something is red then it is young. If something is nice then it is red. If the cow is young and the cow is blue then the cow is nice.
The cow is blue.
("cow" "is" "blue" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If the cow is young and the cow is blue then the cow is nice.
((("cow" "is" "young" "+") ("cow" "is" "blue" "+")) -> ("cow" "is" "nice" "+"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not rough.
False
1
inv-proof
[(triple3)]
("cow" "is" "rough" "-")
triple3
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "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 blue.[(triple1)] The cow is red.[(triple2)] The cow is rough.[(triple3)] @1: The cow is young.[(((triple2) -> rule1))] @2: The cow is nice.[(((((triple2) -> rule1) triple1) -> rule3))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
((triple2) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2