Charlie is cold. Charlie is green. Charlie is round. Charlie is white. Harry is cold. Harry is green. Harry is round. White, round things are furry. If something is furry and smart then it is white. Round, white things are smart. If something is smart then it is rough. If something is round and smart then it is green. Cold things are furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
White, round things are furry.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is furry and smart then it is white.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Round, white things are smart.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is round and smart then it is green.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Charlie is round.
True
1
proof
[(triple3)]
("Charlie" "is" "round" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "round" "-")
triple3
Charlie is furry.
True
2
proof
[(((triple1) -> rule6) OR ((triple4 triple3) -> rule1))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple4 triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not smart.
False
3
inv-proof
[(((triple3 triple4) -> rule3))]
("Charlie" "is" "smart" "-")
((triple3 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@3: Harry is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "white" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2 OR ((triple3 ((triple3 triple4) -> rule3)) -> rule5))] Charlie is round.[(triple3)] Charlie is white.[(triple4)] Harry is cold.[(triple5)] Harry is green.[(triple6)] Harry is round.[(triple7)] @1: Charlie is furry.[(((triple1) -> rule6) OR ((triple4 triple3) -> rule1))] Charlie is smart.[(((triple3 triple4) -> rule3))] Harry is furry.[(((triple5) -> rule6))] @2: Charlie is rough.[(((((triple3 triple4) -> rule3)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple3 ((triple3 triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple4 triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple5) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple3 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2