The dog is red. All kind, rough things are blue. Cold things are red. All kind, cold things are red. If the dog is kind and the dog is red then the dog is cold. If something is red then it is rough. If something is red then it is blue. Red, kind things are blue. If the dog is rough and the dog is blue then the dog is red.
The dog is red.
("dog" "is" "red" "+")
All kind, rough things are blue.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All kind, cold things are red.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If the dog is kind and the dog is red then the dog is cold.
((("dog" "is" "kind" "+") ("dog" "is" "red" "+")) -> ("dog" "is" "cold" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Red, kind things are blue.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If the dog is rough and the dog is blue then the dog is red.
((("dog" "is" "rough" "+") ("dog" "is" "blue" "+")) -> ("dog" "is" "red" "+"))
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 rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("dog" "is" "rough" "-")
((triple1) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "cold" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is red.[(triple1)] @1: The dog is blue.[(((triple1) -> rule6))] The dog is rough.[(((triple1) -> rule5))]
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
The dog is rough.
("dog" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1