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