Anne is quiet. Bob is smart. Erin is rough. If Bob is smart and Bob is round then Bob is kind. Rough things are kind. All quiet, smart things are round. All kind things are round. If Erin is green and Erin is not young then Erin is quiet. All round things are quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If Bob is smart and Bob is round then Bob is kind.
((("Bob" "is" "smart" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "kind" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All quiet, smart things are round.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If Erin is green and Erin is not young then Erin is quiet.
((("Erin" "is" "green" "+") ("Erin" "is" "young" "~")) -> ("Erin" "is" "quiet" "+"))
All round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple3)]
("Erin" "is" "rough" "-")
triple3
Erin is kind.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("Erin" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("Erin" "is" "round" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
True
4
proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule6))]
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule6))]
("Erin" "is" "quiet" "-")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@5: Bob is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- rule4 <- rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is quiet.
Unknown
rconc
[@4: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not round.
Unknown
inv-rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Bob is round.
Unknown
rconc
[@4: Bob is round.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is quiet.[(triple1)] Bob is smart.[(triple2)] Erin is rough.[(triple3)] @1: Erin is kind.[(((triple3) -> rule2))] @2: Erin is round.[(((((triple3) -> rule2)) -> rule4))] @3: Erin is quiet.[(((((((triple3) -> rule2)) -> rule4)) -> rule6))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3