The cow is cold. The cow is kind. The cow is nice. The cow is red. The cow is round. If someone is nice and round then they are cold. Nice people are kind. If the cow is red and the cow is kind then the cow is nice.
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
If someone is nice and round then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If the cow is red and the cow is kind then the cow is nice.
((("cow" "is" "red" "+") ("cow" "is" "kind" "+")) -> ("cow" "is" "nice" "+"))
The cow is red.
True
1
proof
[(triple4)]
("cow" "is" "red" "+")
triple4
The cow is not kind.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule2))]
("cow" "is" "kind" "-")
triple2
((triple3) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "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 cold.[(triple1 OR ((triple3 triple5) -> rule1) OR ((((triple4 triple2) -> rule3) triple5) -> rule1))] The cow is kind.[(triple2 OR ((triple3) -> rule2))] The cow is nice.[(triple3 OR ((triple4 triple2) -> rule3))] The cow is red.[(triple4)] The cow is round.[(triple5)]
The cow is cold.
("cow" "is" "cold" "+")
triple1
((triple3 triple5) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple4 triple2) -> (rule3 % int2)) triple5) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
triple2
((triple3) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
triple3
((triple4 triple2) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5