Anne is blue. Anne is nice. Harry is blue. Harry is not furry. Harry is green. Harry is not red. Harry is rough. Red people are cold. All rough people are cold. If someone is furry and green then they are rough. If Harry is green then Harry is cold. If someone is blue and not cold then they are nice. Cold people are nice. All cold people are nice. If someone is blue then they are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry and green then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Harry is green then Harry is cold.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "cold" "+"))
If someone is blue and not cold then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Harry is not furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "-")
triple4
Harry is not rough.
False
1
inv-proof
[(triple7)]
("Harry" "is" "rough" "-")
triple7
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2 OR ((triple1) -> rule8))] Harry is blue.[(triple3)] Harry is green.[(triple5)] Harry is not furry.[(triple4)] Harry is not red.[(triple6)] Harry is rough.[(triple7)] @1: Harry is cold.[(((triple5) -> rule4) OR ((triple7) -> rule2))] Harry is nice.[(((triple3) -> rule8) OR ((((triple5) -> rule4)) -> rule6) OR ((((triple5) -> rule4)) -> rule7) OR ((((triple7) -> rule2)) -> rule6) OR ((((triple7) -> rule2)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is not furry.
("Harry" "is" "furry" "-")
triple4
Harry is not red.
("Harry" "is" "red" "-")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
((triple5) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2