Anne is kind. Charlie is not big. Erin is kind. Harry is furry. All cold people are smart. If someone is big and not quiet then they are smart. If Anne is not furry then Anne is not cold. All furry people are blue. If someone is quiet and not furry then they are blue. All blue, furry people are cold. All blue people are cold. If Erin is kind and Erin is smart then Erin is not big.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and not quiet then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "smart" "+"))
If Anne is not furry then Anne is not cold.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "cold" "-"))
All furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and not furry then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "blue" "+"))
All blue, furry people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If Erin is kind and Erin is smart then Erin is not big.
((("Erin" "is" "kind" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "big" "-"))
Charlie is not big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "-")
triple2
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Harry is blue.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "-")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
True
3
proof
[(((((triple4) -> rule4)) -> rule7) OR ((((triple4) -> rule4) triple4) -> rule6))]
("Harry" "is" "cold" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule7) OR ((((triple4) -> rule4) triple4) -> rule6))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule1) OR ((((((triple4) -> rule4) triple4) -> rule6)) -> rule1))]
("Harry" "is" "smart" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule1) OR ((((((triple4) -> rule4) triple4) -> rule6)) -> rule1))]
("Harry" "is" "smart" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Erin" "is" "cold" "+")
Anne is not smart.
Unknown
inv-rconc
[@3: Anne is smart.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "-")
Erin is smart.
Unknown
rconc
[@3: Erin is smart.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule4 <- FAIL)]]
("Erin" "is" "smart" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is kind.[(triple1)] Charlie is not big.[(triple2)] Erin is kind.[(triple3)] Harry is furry.[(triple4)] @1: Harry is blue.[(((triple4) -> rule4))] @2: Harry is cold.[(((((triple4) -> rule4)) -> rule7) OR ((((triple4) -> rule4) triple4) -> rule6))] @3: Harry is smart.[(((((((triple4) -> rule4)) -> rule7)) -> rule1) OR ((((((triple4) -> rule4) triple4) -> rule6)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is not big.
("Charlie" "is" "big" "-")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple4) -> (rule4 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3