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