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