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