Bob is green. Bob is quiet. Charlie is kind. Charlie is quiet. Harry is not kind. Harry is nice. Harry is not quiet. If someone is quiet and green then they are white. If someone is red and not nice then they are green. If someone is green and not white then they are furry.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If someone is quiet and green then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is red and not nice then they are green.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "+"))
If someone is green and not white then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "furry" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "quiet" "-")
triple4
Bob is white.
True
3
proof
[(((triple2 triple1) -> rule1))]
("Bob" "is" "white" "+")
((triple2 triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
3
inv-proof
[(((triple2 triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple2 triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is green.[(triple1)] Bob is quiet.[(triple2)] Charlie is kind.[(triple3)] Charlie is quiet.[(triple4)] Harry is nice.[(triple6)] Harry is not kind.[(triple5)] Harry is not quiet.[(triple7)] @1: Bob is white.[(((triple2 triple1) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is not kind.
("Harry" "is" "kind" "-")
triple5
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple2 triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1