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