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