The dog is red. All rough, kind things are red. If something is kind then it is red. If the dog is rough then the dog is red. All cold, rough things are kind. If something is blue and rough then it is kind. All red things are blue.
The dog is red.
("dog" "is" "red" "+")
All rough, kind things are red.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If the dog is rough then the dog is red.
((("dog" "is" "rough" "+")) -> ("dog" "is" "red" "+"))
All cold, rough things are kind.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is blue and rough then it is kind.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
The dog is red.
True
1
proof
[(triple1)]
("dog" "is" "red" "+")
triple1
The dog is not red.
False
1
inv-proof
[(triple1)]
("dog" "is" "red" "-")
triple1
The dog is blue.
True
2
proof
[(((triple1) -> rule6))]
("dog" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("dog" "is" "blue" "-")
((triple1) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "kind" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is red.[(triple1)] @1: The dog is blue.[(((triple1) -> rule6))]
The dog is red.
("dog" "is" "red" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1