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