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