Bob is quiet. Fiona is not blue. All blue things are furry. All kind things are not furry. If something is white and furry then it is blue. If something is quiet then it is blue. If Fiona is nice then Fiona is kind. If something is kind and not white then it is not round.
Bob is quiet.
("Bob" "is" "quiet" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All kind things are not furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "-"))
If something is white and furry then it is blue.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Fiona is nice then Fiona is kind.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "kind" "+"))
If something is kind and not white then it is not round.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "round" "-"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Bob is blue.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is quiet.[(triple1)] Fiona is not blue.[(triple2)] @1: Bob is blue.[(((triple1) -> rule4))] @2: Bob is furry.[(((((triple1) -> rule4)) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2