The cow is green. The cow is kind. The cow is red. The cow is round. The cow is young. All red things are young. If something is young and kind then it is red.
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is young and kind then it is red.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
The cow is young.
True
1
proof
[(triple5 OR ((triple3) -> rule1))]
("cow" "is" "young" "+")
triple5
((triple3) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is not red.
False
1
inv-proof
[(triple3 OR ((triple5 triple2) -> rule2))]
("cow" "is" "red" "-")
triple3
((triple5 triple2) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
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 eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is green.[(triple1)] The cow is kind.[(triple2)] The cow is red.[(triple3 OR ((triple5 triple2) -> rule2))] The cow is round.[(triple4)] The cow is young.[(triple5 OR ((triple3) -> rule1))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
((triple5 triple2) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
((triple3) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1