Anne is nice. Bob is furry. Charlie is kind. Harry is round. If Bob is white then Bob is blue. If something is kind then it is not furry. If something is nice and not white then it is round. Big things are round. All blue things are not kind. If something is big and white then it is kind. If something is nice and not blue then it is not big. If something is round and not blue then it is big.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If Bob is white then Bob is blue.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "blue" "+"))
If something is kind then it is not furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "-"))
If something is nice and not white then it is round.
((("something" "is" "nice" "+") ("something" "is" "white" "~")) -> ("something" "is" "round" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All blue things are not kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
If something is big and white then it is kind.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is nice and not blue then it is not big.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "-"))
If something is round and not blue then it is big.
((("something" "is" "round" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Bob is not furry.
False
1
inv-proof
[(triple2)]
("Bob" "is" "furry" "-")
triple2
Charlie is not furry.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "furry" "-")
((triple3) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is furry.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Bob" "is" "round" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is nice.[(triple1)] Bob is furry.[(triple2)] Charlie is kind.[(triple3)] Harry is round.[(triple4)] @1: Charlie is not furry.[(((triple3) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple3) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1