Anne is cold. Erin is red. If something is kind and quiet then it is round. Cold things are quiet. If Erin is kind and Erin is round then Erin is green. All green, red things are kind. If Erin is round then Erin is rough. If something is cold and green then it is quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
If something is kind and quiet then it is round.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Erin is kind and Erin is round then Erin is green.
((("Erin" "is" "kind" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "green" "+"))
All green, red things are kind.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Erin is round then Erin is rough.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "rough" "+"))
If something is cold and green then it is quiet.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is cold.[(triple1)] Erin is red.[(triple2)] @1: Anne is quiet.[(((triple1) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1