Bob is furry. Bob is quiet. Bob is young. Dave is not cold. Dave is not furry. Dave is quiet. Erin is nice. If someone is blue and not nice then they are not rough. If someone is blue then they are not rough. All nice people are blue.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is blue and not nice then they are not rough.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "rough" "-"))
If someone is blue then they are not rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Erin is nice.
True
1
proof
[(triple7)]
("Erin" "is" "nice" "+")
triple7
Dave is cold.
False
1
inv-proof
[(triple4)]
("Dave" "is" "cold" "+")
triple4
Erin is blue.
True
2
proof
[(((triple7) -> rule3))]
("Erin" "is" "blue" "+")
((triple7) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple7) -> rule3))]
("Erin" "is" "blue" "-")
((triple7) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not rough.
True
3
proof
[(((((triple7) -> rule3)) -> rule2))]
("Erin" "is" "rough" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule2))]
("Erin" "is" "rough" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Bob is furry.[(triple1)] Bob is quiet.[(triple2)] Bob is young.[(triple3)] Dave is not cold.[(triple4)] Dave is not furry.[(triple5)] Dave is quiet.[(triple6)] Erin is nice.[(triple7)] @1: Erin is blue.[(((triple7) -> rule3))] @2: Erin is not rough.[(((((triple7) -> rule3)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is not cold.
("Dave" "is" "cold" "-")
triple4
Dave is not furry.
("Dave" "is" "furry" "-")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
((triple7) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2