The cat is cold. The cat is nice. The cat is not red. The cat is round. The cat is young. If someone is red then they are nice.
The cat is cold.
("cat" "is" "cold" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is not red.
("cat" "is" "red" "-")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
The cat is round.
True
1
proof
[(triple4)]
("cat" "is" "round" "+")
triple4
The cat is not young.
False
1
inv-proof
[(triple5)]
("cat" "is" "young" "-")
triple5
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is cold.[(triple1)] The cat is nice.[(triple2)] The cat is not red.[(triple3)] The cat is round.[(triple4)] The cat is young.[(triple5)]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is not red.
("cat" "is" "red" "-")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5