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