Dave is not furry. Dave is young. Harry is not furry. Young, rough people are white. Furry people are white. All furry, blue people are young. Young people are blue. Blue, young people are rough. Big, furry people are not rough.
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is young.
("Dave" "is" "young" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Young, rough people are white.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All furry, blue people are young.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Blue, young people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Big, furry people are not rough.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "-"))
Dave is not furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Dave is furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is blue.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule5))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule5))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Dave is not furry.[(triple1)] Dave is young.[(triple2)] Harry is not furry.[(triple3)] @1: Dave is blue.[(((triple2) -> rule4))] @2: Dave is rough.[(((((triple2) -> rule4) triple2) -> rule5))] @3: Dave is white.[(((triple2 ((((triple2) -> rule4) triple2) -> rule5)) -> rule1))]
Dave is not furry.
("Dave" "is" "furry" "-")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Harry is not furry.
("Harry" "is" "furry" "-")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple2 ((((triple2) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3