Erin is smart. If Erin is kind then Erin is quiet. Green things are cold. Green things are white. All white, cold things are kind. If something is white and cold then it is green. If something is quiet then it is kind. If something is round then it is quiet. If Erin is smart then Erin is round.
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is kind then Erin is quiet.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All white, cold things are kind.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is white and cold then it is green.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If Erin is smart then Erin is round.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "round" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Erin is not smart.
False
1
inv-proof
[(triple1)]
("Erin" "is" "smart" "-")
triple1
Erin is round.
True
2
proof
[(((triple1) -> rule8))]
("Erin" "is" "round" "+")
((triple1) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("Erin" "is" "round" "-")
((triple1) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("Erin" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Erin" "is" "quiet" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
True
4
proof
[(((((((triple1) -> rule8)) -> rule7)) -> rule6))]
("Erin" "is" "kind" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not kind.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule7)) -> rule6))]
("Erin" "is" "kind" "-")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
@0: Erin is smart.[(triple1)] @1: Erin is round.[(((triple1) -> rule8))] @2: Erin is quiet.[(((((triple1) -> rule8)) -> rule7))] @3: Erin is kind.[(((((((triple1) -> rule8)) -> rule7)) -> rule6))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
((triple1) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3