Anne is kind. Erin is white. Gary is white. Harry is quiet. White, cold people are green. All kind, cold people are green. If Anne is green then Anne is cold. Kind people are cold. Green people are smart. Quiet people are blue.
Anne is kind.
("Anne" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
White, cold people are green.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All kind, cold people are green.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If Anne is green then Anne is cold.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("Anne" "is" "green" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Gary is not smart.
Unknown
inv-rconc
[@3: Gary is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule4 <- FAIL)]]
("Gary" "is" "smart" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "+")
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Erin is white.[(triple2)] Gary is white.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is cold.[(((triple1) -> rule4))] Harry is blue.[(((triple4) -> rule6))] @2: Anne is green.[(((triple1 ((triple1) -> rule4)) -> rule2))] @3: Anne is smart.[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3