Dave is rough. Harry is quiet. Harry is white. If something is furry then it is smart. If something is smart then it is rough. If something is white and quiet then it is furry.
Dave is rough.
("Dave" "is" "rough" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is white and quiet then it is furry.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Harry is quiet.
True
1
proof
[(triple2)]
("Harry" "is" "quiet" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple2)]
("Harry" "is" "quiet" "-")
triple2
Harry is furry.
True
3
proof
[(((triple3 triple2) -> rule3))]
("Harry" "is" "furry" "+")
((triple3 triple2) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
3
inv-proof
[(((triple3 triple2) -> rule3))]
("Harry" "is" "furry" "-")
((triple3 triple2) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
True
4
proof
[(((((triple3 triple2) -> rule3)) -> rule1))]
("Harry" "is" "smart" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple3 triple2) -> rule3)) -> rule1))]
("Harry" "is" "smart" "-")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
True
5
proof
[(((((((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "rough" "+")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not rough.
False
5
inv-proof
[(((((((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "rough" "-")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is rough.[(triple1)] Harry is quiet.[(triple2)] Harry is white.[(triple3)] @1: Harry is furry.[(((triple3 triple2) -> rule3))] @2: Harry is smart.[(((((triple3 triple2) -> rule3)) -> rule1))] @3: Harry is rough.[(((((((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
((triple3 triple2) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3