The cat is big. All big people are kind. If someone is red and not blue then they are not kind. If the cat is blue and the cat is nice then the cat is not red. All kind people are nice. If someone is big and red then they are not nice. If someone is big and kind then they are not red.
The cat is big.
("cat" "is" "big" "+")
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and not blue then they are not kind.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "kind" "-"))
If the cat is blue and the cat is nice then the cat is not red.
((("cat" "is" "blue" "+") ("cat" "is" "nice" "+")) -> ("cat" "is" "red" "-"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and red then they are not nice.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If someone is big and kind then they are not red.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is kind.
True
2
proof
[(((triple1) -> rule1))]
("cat" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
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 is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat is big.[(triple1)] @1: The cat is kind.[(((triple1) -> rule1))] @2: The cat is nice.[(((((triple1) -> rule1)) -> rule4))] The cat is not red.[(((triple1 ((triple1) -> rule1)) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is not red.
("cat" "is" "red" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cat is not red.
("cat" "is" "red" "-")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2