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