Anne is smart. Bob is smart. Erin is not white. Fiona is not rough. All smart things are cold. If Erin is not quiet and Erin is not rough then Erin is not smart. All cold things are furry.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
Fiona is not rough.
("Fiona" "is" "rough" "-")
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Erin is not quiet and Erin is not rough then Erin is not smart.
((("Erin" "is" "quiet" "~") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "smart" "-"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Erin is not white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is furry.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is smart.[(triple1)] Bob is smart.[(triple2)] Erin is not white.[(triple3)] Fiona is not rough.[(triple4)] @1: Anne is cold.[(((triple1) -> rule1))] Bob is cold.[(((triple2) -> rule1))] @2: Anne is furry.[(((((triple1) -> rule1)) -> rule3))] Bob is furry.[(((((triple2) -> rule1)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is not white.
("Erin" "is" "white" "-")
triple3
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2