Charlie is nice. Dave is round. Harry is not white. If Dave is big then Dave is round. If someone is big then they are round. Round people are nice. If Charlie is red and Charlie is nice then Charlie is white. If someone is round and not big then they are not red. If someone is green and not round then they are white. If Harry is not nice then Harry is white. If someone is red and not white then they are quiet.
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is not white.
("Harry" "is" "white" "-")
If Dave is big then Dave is round.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "round" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is red and Charlie is nice then Charlie is white.
((("Charlie" "is" "red" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "white" "+"))
If someone is round and not big then they are not red.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "red" "-"))
If someone is green and not round then they are white.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "white" "+"))
If Harry is not nice then Harry is white.
((("Harry" "is" "nice" "~")) -> ("Harry" "is" "white" "+"))
If someone is red and not white then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
Harry is not white.
True
1
proof
[(triple3)]
("Harry" "is" "white" "-")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Dave is nice.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "round" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is nice.[(triple1)] Dave is round.[(triple2)] Harry is not white.[(triple3)] @1: Dave is nice.[(((triple2) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Harry is not white.
("Harry" "is" "white" "-")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1