Charlie is cold. Charlie is furry. Charlie is green. Gary is not big. Gary is green. Gary is not rough. Harry is big. Harry is blue. Harry is cold. Harry is green. Harry is red. Harry is rough. If something is rough and not red then it is green. Rough, big things are green. If Harry is not red then Harry is not rough. If Charlie is not red then Charlie is not big. If something is cold and not furry then it is blue. If something is green and not big then it is blue.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is not 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 blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is rough and not red then it is green.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "+"))
Rough, big things are green.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Harry is not red then Harry is not rough.
((("Harry" "is" "red" "~")) -> ("Harry" "is" "rough" "-"))
If Charlie is not red then Charlie is not big.
((("Charlie" "is" "red" "~")) -> ("Charlie" "is" "big" "-"))
If something is cold and not furry then it is blue.
((("something" "is" "cold" "+") ("something" "is" "furry" "~")) -> ("something" "is" "blue" "+"))
If something is green and not big then it is blue.
((("something" "is" "green" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "+"))
Harry is green.
True
1
proof
[(triple10 OR ((triple12 triple7) -> rule2))]
("Harry" "is" "green" "+")
triple10
((triple12 triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Gary is rough.
False
1
inv-proof
[(triple6)]
("Gary" "is" "rough" "+")
triple6
Gary is blue.
True
3
proof
[(((triple5 triple4) -> rule6))]
("Gary" "is" "blue" "+")
((triple5 triple4) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
3
inv-proof
[(((triple5 triple4) -> rule6))]
("Gary" "is" "blue" "-")
((triple5 triple4) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Gary is green.[(triple5)] Gary is not big.[(triple4)] Gary is not rough.[(triple6)] Harry is big.[(triple7)] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is green.[(triple10 OR ((triple12 triple7) -> rule2))] Harry is red.[(triple11)] Harry is rough.[(triple12)] @1: Gary is blue.[(((triple5 triple4) -> rule6))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is not big.
("Gary" "is" "big" "-")
triple4
Gary is not rough.
("Gary" "is" "rough" "-")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
((triple12 triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
((triple5 triple4) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1