Anne is white. Dave is cold. Erin is round. Harry is blue. Harry is cold. Harry is white. Harry is young. If someone is kind and young then they are red. If Dave is round and Dave is cold then Dave is white. If someone is young then they are red. Kind people are blue. Blue people are kind. If Erin is kind then Erin is white.
Anne is white.
("Anne" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is kind and young then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Dave is round and Dave is cold then Dave is white.
((("Dave" "is" "round" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "white" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Erin is kind then Erin is white.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "white" "+"))
Erin is round.
True
1
proof
[(triple3)]
("Erin" "is" "round" "+")
triple3
Harry is not cold.
False
1
inv-proof
[(triple5)]
("Harry" "is" "cold" "-")
triple5
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule4 <- FAIL)]]
("Erin" "is" "white" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is white.[(triple1)] Dave is cold.[(triple2)] Erin is round.[(triple3)] Harry is blue.[(triple4)] Harry is cold.[(triple5)] Harry is white.[(triple6)] Harry is young.[(triple7)] @1: Harry is kind.[(((triple4) -> rule5))] Harry is red.[(((triple7) -> rule3) OR ((((triple4) -> rule5) triple7) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple7) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple4) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2