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