Anne is not kind. Erin is furry. Harry is furry. If something is round and not green then it is not kind. If something is round then it is smart. All kind things are smart. If something is green then it is not smart. If something is kind and not green then it is not furry. All green, kind things are furry. If something is furry then it is cold. All cold things are round.
Anne is not kind.
("Anne" "is" "kind" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is round and not green then it is not kind.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "-"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is green then it is not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
If something is kind and not green then it is not furry.
((("something" "is" "kind" "+") ("something" "is" "green" "~")) -> ("something" "is" "furry" "-"))
All green, kind things are furry.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Anne is kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Harry is cold.
True
2
proof
[(((triple3) -> rule7))]
("Harry" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "cold" "-")
((triple2) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is round.
True
3
proof
[(((((triple3) -> rule7)) -> rule8))]
("Harry" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule8))]
("Erin" "is" "round" "-")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
True
4
proof
[(((((((triple2) -> rule7)) -> rule8)) -> rule2))]
("Erin" "is" "smart" "+")
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule8)) -> rule2))]
("Harry" "is" "smart" "-")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is round.
Unknown
rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule6 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is smart.
Unknown
rconc
[@4: Anne is smart.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule7 <- rule6 <- FAIL)]]
("Anne" "is" "smart" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is not kind.[(triple1)] Erin is furry.[(triple2)] Harry is furry.[(triple3)] @1: Erin is cold.[(((triple2) -> rule7))] Harry is cold.[(((triple3) -> rule7))] @2: Erin is round.[(((((triple2) -> rule7)) -> rule8))] Harry is round.[(((((triple3) -> rule7)) -> rule8))] @3: Erin is smart.[(((((((triple2) -> rule7)) -> rule8)) -> rule2))] Harry is smart.[(((((((triple3) -> rule7)) -> rule8)) -> rule2))]
Anne is not kind.
("Anne" "is" "kind" "-")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3