Bob is young. Dave is blue. Erin is blue. If Bob is red and Bob is white then Bob is cold. If someone is blue and red then they are kind. All blue people are not kind. If someone is cold and not young then they are quiet. If Bob is blue then Bob is quiet. If Bob is not red then Bob is blue.
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is blue.
("Erin" "is" "blue" "+")
If Bob is red and Bob is white then Bob is cold.
((("Bob" "is" "red" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "cold" "+"))
If someone is blue and red then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All blue people are not kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "-"))
If someone is cold and not young then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "quiet" "+"))
If Bob is blue then Bob is quiet.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "quiet" "+"))
If Bob is not red then Bob is blue.
((("Bob" "is" "red" "~")) -> ("Bob" "is" "blue" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Erin is not kind.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is kind.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is young.[(triple1)] Dave is blue.[(triple2)] Erin is blue.[(triple3)] @1: Dave is not kind.[(((triple2) -> rule3))] Erin is not kind.[(((triple3) -> rule3))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Dave is not kind.
("Dave" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1