Anne is blue. Dave is cold. Erin is not cold. Erin is not green. Erin is nice. Harry is nice. Harry is not red. If something is green and nice then it is quiet. Nice, cold things are not blue. All blue things are nice. If Harry is white then Harry is not red. If something is quiet then it is green. Red things are green. If something is blue and cold then it is green. Green, cold things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not green.
("Erin" "is" "green" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
If something is green and nice then it is quiet.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Nice, cold things are not blue.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If Harry is white then Harry is not red.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "red" "-"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is blue and cold then it is green.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Green, cold things are white.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple6)]
("Harry" "is" "nice" "+")
triple6
Erin is not nice.
False
1
inv-proof
[(triple5)]
("Erin" "is" "nice" "-")
triple5
Anne is nice.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "white" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is blue.[(triple1)] Dave is cold.[(triple2)] Erin is nice.[(triple5)] Erin is not cold.[(triple3)] Erin is not green.[(triple4)] Harry is nice.[(triple6)] Harry is not red.[(triple7)] @1: Anne is nice.[(((triple1) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is not cold.
("Erin" "is" "cold" "-")
triple3
Erin is not green.
("Erin" "is" "green" "-")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is not red.
("Harry" "is" "red" "-")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1