Charlie is cold. Erin is smart. Gary is furry. Harry is nice. Big things are nice. All smart, furry things are kind. Kind, smart things are furry. If something is cold and nice then it is big. If something is big then it is smart. If Charlie is nice and Charlie is kind then Charlie is cold. If something is furry then it is big. All cold things are kind.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All smart, furry things are kind.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Kind, smart things are furry.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is cold and nice then it is big.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Charlie is nice and Charlie is kind then Charlie is cold.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Gary is furry.
True
1
proof
[(triple3)]
("Gary" "is" "furry" "+")
triple3
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Gary is big.
True
2
proof
[(((triple3) -> rule7))]
("Gary" "is" "big" "+")
((triple3) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule8))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is smart.
True
3
proof
[(((((triple3) -> rule7)) -> rule5))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule1))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
True
5
proof
[(((((((triple3) -> rule7)) -> rule5) triple3) -> rule2))]
("Gary" "is" "kind" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not kind.
False
5
inv-proof
[(((((((triple3) -> rule7)) -> rule5) triple3) -> rule2))]
("Gary" "is" "kind" "-")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Charlie is nice.
Unknown
rconc
[@5: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule3 <- rule5 <- rule4 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not big.
Unknown
inv-rconc
[@5: Charlie is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is smart.
Unknown
rconc
[@5: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- rule7 <- rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] Erin is smart.[(triple2)] Gary is furry.[(triple3)] Harry is nice.[(triple4)] @1: Charlie is kind.[(((triple1) -> rule8))] Gary is big.[(((triple3) -> rule7))] @2: Gary is nice.[(((((triple3) -> rule7)) -> rule1))] Gary is smart.[(((((triple3) -> rule7)) -> rule5))] @3: Gary is kind.[(((((((triple3) -> rule7)) -> rule5) triple3) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3