Charlie is cold. Charlie is young. Dave is big. Dave is cold. Dave is furry. Dave is green. Dave is not rough. Dave is not young. Gary is big. Gary is green. Gary is not rough. Harry is big. Harry is furry. Harry is green. Harry is rough. Harry is young. If something is cold and furry then it is green. If something is big and young then it is green. If something is furry then it is smart.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is not young.
("Dave" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is cold and furry then it is green.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is big and young then it is green.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Harry is young.
True
1
proof
[(triple16)]
("Harry" "is" "young" "+")
triple16
Gary is not green.
False
1
inv-proof
[(triple10)]
("Gary" "is" "green" "-")
triple10
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is cold.[(triple1)] Charlie is young.[(triple2)] Dave is big.[(triple3)] Dave is cold.[(triple4)] Dave is furry.[(triple5)] Dave is green.[(triple6 OR ((triple4 triple5) -> rule1))] Dave is not rough.[(triple7)] Dave is not young.[(triple8)] Gary is big.[(triple9)] Gary is green.[(triple10)] Gary is not rough.[(triple11)] Harry is big.[(triple12)] Harry is furry.[(triple13)] Harry is green.[(triple14 OR ((triple12 triple16) -> rule2))] Harry is rough.[(triple15)] Harry is young.[(triple16)] @1: Dave is smart.[(((triple5) -> rule3))] Harry is smart.[(((triple13) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
((triple4 triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is not young.
("Dave" "is" "young" "-")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is not rough.
("Gary" "is" "rough" "-")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
((triple12 triple16) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple13) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1