The cow is big. The cow is blue. The cow is kind. The cow is nice. The cow is red. All blue, nice people are kind. All big, nice people are red.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
All blue, nice people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All big, nice people are red.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
The cow is big.
True
1
proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The cow is not kind.
False
1
inv-proof
[(triple3 OR ((triple2 triple4) -> rule1))]
("cow" "is" "kind" "-")
triple3
((triple2 triple4) -> (rule1 % 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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is big.[(triple1)] The cow is blue.[(triple2)] The cow is kind.[(triple3 OR ((triple2 triple4) -> rule1))] The cow is nice.[(triple4)] The cow is red.[(triple5 OR ((triple1 triple4) -> rule2))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
((triple2 triple4) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
((triple1 triple4) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1