Dave is not rough. Harry is big. All green things are not rough. All big things are green. All young, furry things are not green.
Dave is not rough.
("Dave" "is" "rough" "-")
Harry is big.
("Harry" "is" "big" "+")
All green things are not rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "-"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All young, furry things are not green.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "-"))
Dave is not rough.
True
1
proof
[(triple1)]
("Dave" "is" "rough" "-")
triple1
Dave is rough.
False
1
inv-proof
[(triple1)]
("Dave" "is" "rough" "+")
triple1
Harry is green.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "green" "-")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not rough.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Harry" "is" "rough" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Harry" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is not rough.[(triple1)] Harry is big.[(triple2)] @1: Harry is green.[(((triple2) -> rule2))] @2: Harry is not rough.[(((((triple2) -> rule2)) -> rule1))]
Dave is not rough.
("Dave" "is" "rough" "-")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2