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