Bob is blue. Bob is nice. Bob is quiet. Bob is rough. Bob is white. Charlie is furry. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is white. Harry is red. Harry is white. All white people are nice. If someone is furry then they are white. If Harry is red and Harry is blue then Harry is quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Harry is red and Harry is blue then Harry is quiet.
((("Harry" "is" "red" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "quiet" "+"))
Charlie is nice.
True
1
proof
[(triple7 OR ((triple10) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Charlie" "is" "nice" "+")
triple7
((triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not nice.
False
1
inv-proof
[(triple7 OR ((triple10) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Charlie" "is" "nice" "-")
triple7
((triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2 OR ((triple5) -> rule1))] Bob is quiet.[(triple3)] Bob is rough.[(triple4)] Bob is white.[(triple5)] Charlie is furry.[(triple6)] Charlie is nice.[(triple7 OR ((triple10) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Charlie is quiet.[(triple8)] Charlie is red.[(triple9)] Charlie is white.[(triple10 OR ((triple6) -> rule2))] Harry is red.[(triple11)] Harry is white.[(triple12)] @1: Harry is nice.[(((triple12) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
((triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
((triple6) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1