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