The cat is cold. The cat is kind. The cat is nice. All cold people are red. If someone is cold then they are red. All red people are nice.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
The cat is nice.
True
1
proof
[(triple3 OR ((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule2)) -> rule3))]
("cat" "is" "nice" "+")
triple3
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not nice.
False
1
inv-proof
[(triple3 OR ((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule2)) -> rule3))]
("cat" "is" "nice" "-")
triple3
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
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 kind.[(triple2)] The cat is nice.[(triple3 OR ((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule2)) -> rule3))] @1: The cat is red.[(((triple1) -> rule1) OR ((triple1) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1