Erin is smart. All white things are round. All big, quiet things are white. Big things are cold. All round things are cold. All smart things are round. If Erin is white then Erin is red.
Erin is smart.
("Erin" "is" "smart" "+")
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All big, quiet things are white.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Erin is white then Erin is red.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "red" "+"))
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) -> rule5))]
("Erin" "is" "round" "+")
((triple1) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Erin" "is" "round" "-")
((triple1) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is red.
Unknown
rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Erin is smart.[(triple1)] @1: Erin is round.[(((triple1) -> rule5))] @2: Erin is cold.[(((((triple1) -> rule5)) -> rule4))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
((triple1) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2