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