Charlie is young. Erin is cold. Gary is rough. If Charlie is furry and Charlie is young then Charlie is red. All rough people are kind. Red people are kind. All red people are rough. If someone is cold and young then they are kind. If Charlie is cold and Charlie is rough then Charlie is red. If Erin is red then Erin is white. If someone is kind then they are red.
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Charlie is furry and Charlie is young then Charlie is red.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "red" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and young then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is cold and Charlie is rough then Charlie is red.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "red" "+"))
If Erin is red then Erin is white.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "white" "+"))
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Gary is kind.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Charlie is red.
Unknown
rconc
[@4: Charlie is red.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Charlie is young.[(triple1)] Erin is cold.[(triple2)] Gary is rough.[(triple3)] @1: Gary is kind.[(((triple3) -> rule2))] @2: Gary is red.[(((((triple3) -> rule2)) -> rule8))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2