Charlie is furry. Charlie is kind. Charlie is smart. Charlie is young. Gary is not cold. Gary is kind. Gary is not nice. Gary is not young. Harry is blue. Harry is smart. If something is blue then it is furry. All furry, smart things are nice.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is not young.
("Gary" "is" "young" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All furry, smart things are nice.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is nice.
True
3
proof
[(((triple1 triple3) -> rule2))]
("Charlie" "is" "nice" "+")
((triple1 triple3) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple9) -> rule1))]
("Harry" "is" "furry" "-")
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
True
4
proof
[(((((triple9) -> rule1) triple10) -> rule2))]
("Harry" "is" "nice" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((((triple9) -> rule1) triple10) -> rule2))]
("Harry" "is" "nice" "-")
((((triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is furry.[(triple1)] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] Charlie is young.[(triple4)] Gary is kind.[(triple6)] Gary is not cold.[(triple5)] Gary is not nice.[(triple7)] Gary is not young.[(triple8)] Harry is blue.[(triple9)] Harry is smart.[(triple10)] @1: Charlie is nice.[(((triple1 triple3) -> rule2))] Harry is furry.[(((triple9) -> rule1))] @2: Harry is nice.[(((((triple9) -> rule1) triple10) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is not nice.
("Gary" "is" "nice" "-")
triple7
Gary is not young.
("Gary" "is" "young" "-")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1 triple3) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2