The cat is kind. The cat is nice. The cat is round. Young, big things are round. If the cat is nice then the cat is young. If the cat is big then the cat is young.
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
Young, big things are round.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If the cat is nice then the cat is young.
((("cat" "is" "nice" "+")) -> ("cat" "is" "young" "+"))
If the cat is big then the cat is young.
((("cat" "is" "big" "+")) -> ("cat" "is" "young" "+"))
The cat is nice.
True
1
proof
[(triple2)]
("cat" "is" "nice" "+")
triple2
The cat is not nice.
False
1
inv-proof
[(triple2)]
("cat" "is" "nice" "-")
triple2
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is kind.[(triple1)] The cat is nice.[(triple2)] The cat is round.[(triple3)] @1: The cat is young.[(((triple2) -> rule2))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
((triple2) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1