The cat is big. The cat is not cold. The cat is not kind. The cat is nice. The cat is round. Big, nice people are not cold. All cold people are round. If someone is nice and round then they are not kind.
The cat is big.
("cat" "is" "big" "+")
The cat is not cold.
("cat" "is" "cold" "-")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
Big, nice people are not cold.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "-"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and round then they are not kind.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "-"))
The cat is nice.
True
1
proof
[(triple4)]
("cat" "is" "nice" "+")
triple4
The cat is not nice.
False
1
inv-proof
[(triple4)]
("cat" "is" "nice" "-")
triple4
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is big.[(triple1)] The cat is nice.[(triple4)] The cat is not cold.[(triple2 OR ((triple1 triple4) -> rule1))] The cat is not kind.[(triple3 OR ((triple4 triple5) -> rule3))] The cat is round.[(triple5)]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is not cold.
("cat" "is" "cold" "-")
triple2
((triple1 triple4) -> (rule1 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat is not kind.
("cat" "is" "kind" "-")
triple3
((triple4 triple5) -> (rule3 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is round.
("cat" "is" "round" "+")
triple5