Anne is not blue. Charlie is blue. Gary is red. Cold, rough things are not white. All rough things are white. Rough things are kind. Young, white things are not cold. If something is blue then it is not cold. If something is white and rough then it is blue. If something is blue then it is red. Rough things are young.
Anne is not blue.
("Anne" "is" "blue" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Cold, rough things are not white.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "-"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Young, white things are not cold.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
If something is blue then it is not cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
If something is white and rough then it is blue.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Charlie is red.
True
2
proof
[(((triple2) -> rule7))]
("Charlie" "is" "red" "+")
((triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple2) -> rule7))]
("Charlie" "is" "red" "-")
((triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is not blue.[(triple1)] Charlie is blue.[(triple2)] Gary is red.[(triple3)] @1: Charlie is not cold.[(((triple2) -> rule5))] Charlie is red.[(((triple2) -> rule7))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple2) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1