Anne is nice. Erin is cold. Fiona is blue. Harry is red. If Anne is blue and Anne is kind then Anne is nice. If something is red then it is cold. If something is blue and not cold then it is white.
Anne is nice.
("Anne" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
If Anne is blue and Anne is kind then Anne is nice.
((("Anne" "is" "blue" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "nice" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is blue and not cold then it is white.
((("something" "is" "blue" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "+"))
Harry is red.
True
1
proof
[(triple4)]
("Harry" "is" "red" "+")
triple4
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Harry is cold.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "cold" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is nice.[(triple1)] Erin is cold.[(triple2)] Fiona is blue.[(triple3)] Harry is red.[(triple4)] @1: Harry is cold.[(((triple4) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1