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