Harry is nice. If something is round then it is big. All round, kind things are big. If something is furry then it is big. All furry, round things are blue. Nice things are round. If something is kind then it is green. Furry things are nice. If something is nice and blue then it is furry.
Harry is nice.
("Harry" "is" "nice" "+")
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All round, kind things are big.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All furry, round things are blue.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is nice and blue then it is furry.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Harry is nice.
True
1
proof
[(triple1)]
("Harry" "is" "nice" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple1)]
("Harry" "is" "nice" "-")
triple1
Harry is round.
True
2
proof
[(((triple1) -> rule5))]
("Harry" "is" "round" "+")
((triple1) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Harry" "is" "round" "-")
((triple1) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Harry" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Harry" "is" "big" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Harry is nice.[(triple1)] @1: Harry is round.[(((triple1) -> rule5))] @2: Harry is big.[(((((triple1) -> rule5)) -> rule1))]
Harry is nice.
("Harry" "is" "nice" "+")
triple1
Harry is round.
("Harry" "is" "round" "+")
((triple1) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2