Dave is big. Harry is white. If Dave is big then Dave is quiet. All big, blue things are quiet. If something is quiet then it is furry. Blue things are white. If Dave is smart and Dave is big then Dave is furry. Big things are white.
Dave is big.
("Dave" "is" "big" "+")
Harry is white.
("Harry" "is" "white" "+")
If Dave is big then Dave is quiet.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "quiet" "+"))
All big, blue things are quiet.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Dave is smart and Dave is big then Dave is furry.
((("Dave" "is" "smart" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "furry" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Harry is white.
True
1
proof
[(triple2)]
("Harry" "is" "white" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is white.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "white" "+")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "furry" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is big.[(triple1)] Harry is white.[(triple2)] @1: Dave is quiet.[(((triple1) -> rule1))] Dave is white.[(((triple1) -> rule6))] @2: Dave is furry.[(((((triple1) -> rule1)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2