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