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