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