The cat is nice. The cat is rough. The cat is round. All rough, red things are kind. If the cat is round and the cat is kind then the cat is red. Nice things are red.
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
All rough, red things are kind.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If the cat is round and the cat is kind then the cat is red.
((("cat" "is" "round" "+") ("cat" "is" "kind" "+")) -> ("cat" "is" "red" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple2)]
("cat" "is" "rough" "-")
triple2
The cat is red.
True
2
proof
[(((triple1) -> rule3))]
("cat" "is" "red" "+")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "is" "red" "-")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
True
4
proof
[(((triple2 ((triple1) -> rule3)) -> rule1))]
("cat" "is" "kind" "+")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not kind.
False
4
inv-proof
[(((triple2 ((triple1) -> rule3)) -> rule1))]
("cat" "is" "kind" "-")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
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 likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is nice.[(triple1)] The cat is rough.[(triple2)] The cat is round.[(triple3)] @1: The cat is red.[(((triple1) -> rule3))] @2: The cat is kind.[(((triple2 ((triple1) -> rule3)) -> rule1))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2