Bob is furry. Erin is furry. Fiona is round. Gary is round. If something is round then it is rough. If something is rough then it is furry. Big, furry things are green.
Bob is furry.
("Bob" "is" "furry" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Big, furry things are green.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Fiona is rough.
True
2
proof
[(((triple3) -> rule1))]
("Fiona" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "rough" "-")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "furry" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Fiona is not furry.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Fiona" "is" "furry" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is furry.[(triple1)] Erin is furry.[(triple2)] Fiona is round.[(triple3)] Gary is round.[(triple4)] @1: Fiona is rough.[(((triple3) -> rule1))] Gary is rough.[(((triple4) -> rule1))] @2: Fiona is furry.[(((((triple3) -> rule1)) -> rule2))] Gary is furry.[(((((triple4) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2