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