Anne is cold. Anne is nice. Anne is rough. Dave is cold. Dave is rough. Dave is round. Dave is young. Erin is big. Erin is cold. Erin is young. All rough, furry people are big. Round people are rough. If someone is cold and rough then they are furry. If someone is furry then they are nice. All young, rough people are furry. All big people are young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
All rough, furry people are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and rough then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All young, rough people are furry.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Erin is big.
True
1
proof
[(triple8)]
("Erin" "is" "big" "+")
triple8
Erin is not big.
False
1
inv-proof
[(triple8)]
("Erin" "is" "big" "-")
triple8
Dave is furry.
True
3
proof
[(((triple4 triple5) -> rule3) OR ((triple7 triple5) -> rule5) OR ((triple4 ((triple6) -> rule2)) -> rule3) OR ((triple7 ((triple6) -> rule2)) -> rule5))]
("Dave" "is" "furry" "+")
((triple4 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple7 triple5) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple4 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple7 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((triple4 triple5) -> rule3) OR ((triple7 triple5) -> rule5) OR ((triple4 ((triple6) -> rule2)) -> rule3) OR ((triple7 ((triple6) -> rule2)) -> rule5))]
("Dave" "is" "furry" "-")
((triple4 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple7 triple5) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple4 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple7 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
True
4
proof
[(((((triple4 triple5) -> rule3)) -> rule4) OR ((((triple7 triple5) -> rule5)) -> rule4) OR ((((triple4 ((triple6) -> rule2)) -> rule3)) -> rule4) OR ((((triple7 ((triple6) -> rule2)) -> rule5)) -> rule4))]
("Dave" "is" "nice" "+")
((((triple4 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple7 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple4 ((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple7 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Anne is not big.
False
5
inv-proof
[(((triple3 ((triple1 triple3) -> rule3)) -> rule1))]
("Anne" "is" "big" "-")
((triple3 ((triple1 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is furry.
Unknown
rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not nice.
Unknown
inv-rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2 OR ((((triple1 triple3) -> rule3)) -> rule4))] Anne is rough.[(triple3)] Dave is cold.[(triple4)] Dave is rough.[(triple5 OR ((triple6) -> rule2))] Dave is round.[(triple6)] Dave is young.[(triple7 OR ((((triple5 ((triple4 triple5) -> rule3)) -> rule1)) -> rule6) OR ((((((triple6) -> rule2) ((triple4 triple5) -> rule3)) -> rule1)) -> rule6) OR ((((triple5 ((triple4 ((triple6) -> rule2)) -> rule3)) -> rule1)) -> rule6) OR ((((((triple6) -> rule2) ((triple4 ((triple6) -> rule2)) -> rule3)) -> rule1)) -> rule6))] Erin is big.[(triple8)] Erin is cold.[(triple9)] Erin is young.[(triple10 OR ((triple8) -> rule6))] @1: Anne is furry.[(((triple1 triple3) -> rule3))] Dave is furry.[(((triple4 triple5) -> rule3) OR ((triple7 triple5) -> rule5) OR ((triple4 ((triple6) -> rule2)) -> rule3) OR ((triple7 ((triple6) -> rule2)) -> rule5))] @2: Anne is big.[(((triple3 ((triple1 triple3) -> rule3)) -> rule1))] Dave is big.[(((triple5 ((triple4 triple5) -> rule3)) -> rule1) OR ((triple5 ((triple7 triple5) -> rule5)) -> rule1) OR ((((triple6) -> rule2) ((triple4 triple5) -> rule3)) -> rule1) OR ((((triple6) -> rule2) ((triple7 triple5) -> rule5)) -> rule1) OR ((triple5 ((triple4 ((triple6) -> rule2)) -> rule3)) -> rule1) OR ((triple5 ((triple7 ((triple6) -> rule2)) -> rule5)) -> rule1) OR ((((triple6) -> rule2) ((triple4 ((triple6) -> rule2)) -> rule3)) -> rule1) OR ((((triple6) -> rule2) ((triple7 ((triple6) -> rule2)) -> rule5)) -> rule1))] Dave is nice.[(((((triple4 triple5) -> rule3)) -> rule4) OR ((((triple7 triple5) -> rule5)) -> rule4) OR ((((triple4 ((triple6) -> rule2)) -> rule3)) -> rule4) OR ((((triple7 ((triple6) -> rule2)) -> rule5)) -> rule4))] @3: Anne is young.[(((((triple3 ((triple1 triple3) -> rule3)) -> rule1)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((((triple1 triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple6) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((((triple5 ((triple4 triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((triple6) -> (rule2 % int4)) ((triple4 triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple5 ((triple4 ((triple6) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((triple6) -> (rule2 % int4)) ((triple4 ((triple6) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple8) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 triple3) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple4 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple7 triple5) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple4 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple7 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple3 ((triple1 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple5 ((triple4 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple5 ((triple7 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple4 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple6) -> (rule2 % int3)) ((triple7 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple5 ((triple4 ((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple5 ((triple7 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple6) -> (rule2 % int3)) ((triple4 ((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple6) -> (rule2 % int3)) ((triple7 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple7 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple4 ((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple7 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((triple3 ((triple1 triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3