Bob is blue. Dave is green. Erin is furry. Fiona is not furry. If something is young then it is not furry. If something is green then it is nice. If something is blue then it is rough.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
If something is young then it is not furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "-"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Fiona is furry.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "furry" "+")
triple4
Dave is nice.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "nice" "-")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Dave is green.[(triple2)] Erin is furry.[(triple3)] Fiona is not furry.[(triple4)] @1: Bob is rough.[(((triple1) -> rule3))] Dave is nice.[(((triple2) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1