The cow is blue. The cow is green. The cow is nice. The cow is rough. The cow is round. If something is green and nice then it is rough. If the cow is rough and the cow is green then the cow is blue. All rough things are nice.
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
If something is green and nice then it is rough.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If the cow is rough and the cow is green then the cow is blue.
((("cow" "is" "rough" "+") ("cow" "is" "green" "+")) -> ("cow" "is" "blue" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
The cow is blue.
True
1
proof
[(triple1 OR ((triple4 triple2) -> rule2) OR ((((triple2 triple3) -> rule1) triple2) -> rule2))]
("cow" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is not nice.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule3))]
("cow" "is" "nice" "-")
triple3
((triple4) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
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 OR ((triple4 triple2) -> rule2) OR ((((triple2 triple3) -> rule1) triple2) -> rule2))] The cow is green.[(triple2)] The cow is nice.[(triple3 OR ((triple4) -> rule3))] The cow is rough.[(triple4 OR ((triple2 triple3) -> rule1))] The cow is round.[(triple5)]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
((triple4) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
triple4
((triple2 triple3) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple5