Bob is blue. Bob is kind. Bob is nice. Bob is quiet. Bob is red. Bob is smart. Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is smart. Gary is blue. Gary is nice. Harry is green. Harry is smart. If Dave is kind then Dave is nice. If Bob is green then Bob is kind. If Gary is nice then Gary is green. If Harry is green then Harry is quiet. Red people are blue. If Harry is green and Harry is nice then Harry is quiet. If Harry is quiet then Harry is green. If Bob is red and Bob is kind then Bob is quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Dave is kind then Dave is nice.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "nice" "+"))
If Bob is green then Bob is kind.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "kind" "+"))
If Gary is nice then Gary is green.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "green" "+"))
If Harry is green then Harry is quiet.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "quiet" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Harry is green and Harry is nice then Harry is quiet.
((("Harry" "is" "green" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
If Harry is quiet then Harry is green.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
If Bob is red and Bob is kind then Bob is quiet.
((("Bob" "is" "red" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "quiet" "+"))
Dave is kind.
True
1
proof
[(triple7)]
("Dave" "is" "kind" "+")
triple7
Bob is not blue.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule5))]
("Bob" "is" "blue" "-")
triple1
((triple5) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is blue.[(triple1 OR ((triple5) -> rule5))] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4 OR ((triple5 triple2) -> rule8))] Bob is red.[(triple5)] Bob is smart.[(triple6)] Dave is kind.[(triple7)] Dave is nice.[(triple8 OR ((triple7) -> rule1))] Dave is quiet.[(triple9)] Dave is red.[(triple10)] Dave is smart.[(triple11)] Gary is blue.[(triple12)] Gary is nice.[(triple13)] Harry is green.[(triple14)] Harry is smart.[(triple15)] @1: Dave is blue.[(((triple10) -> rule5))] Gary is green.[(((triple13) -> rule3))] Harry is quiet.[(((triple14) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple5 triple2) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple7) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Dave is blue.
("Dave" "is" "blue" "+")
((triple10) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple13) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple14) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1