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