Anne is quiet. Anne is round. Erin is cold. Harry is cold. Harry is furry. Harry is round. Harry is young. Nice, red things are round. Young things are quiet. All round, red things are quiet. If Erin is round then Erin is red. If something is young and round then it is cold. All quiet things are nice. All young, red things are quiet. If Erin is nice then Erin is red.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Nice, red things are round.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All round, red things are quiet.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Erin is round then Erin is red.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "red" "+"))
If something is young and round then it is cold.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All young, red things are quiet.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Erin is nice then Erin is red.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "red" "+"))
Harry is furry.
True
1
proof
[(triple5)]
("Harry" "is" "furry" "+")
triple5
Harry is not cold.
False
1
inv-proof
[(triple4 OR ((triple7 triple6) -> rule5))]
("Harry" "is" "cold" "-")
triple4
((triple7 triple6) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@4: Erin is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is quiet.[(triple1)] Anne is round.[(triple2)] Erin is cold.[(triple3)] Harry is cold.[(triple4 OR ((triple7 triple6) -> rule5))] Harry is furry.[(triple5)] Harry is round.[(triple6)] Harry is young.[(triple7)] @1: Anne is nice.[(((triple1) -> rule6))] Harry is quiet.[(((triple7) -> rule2))] @2: Harry is nice.[(((((triple7) -> rule2)) -> rule6))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
((triple7 triple6) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2