Dave is not quiet. Dave is red. Dave is young. Harry is furry. Harry is quiet. Harry is not round. Harry is not young. If Harry is young then Harry is round. Young people are big. If someone is young and big then they are furry. If Dave is red and Dave is not round then Dave is big. If Harry is not furry then Harry is not red. If someone is white and young then they are not quiet. Red, furry people are not white. Quiet people are not white.
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is not young.
("Harry" "is" "young" "-")
If Harry is young then Harry is round.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "round" "+"))
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is young and big then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Dave is red and Dave is not round then Dave is big.
((("Dave" "is" "red" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "big" "+"))
If Harry is not furry then Harry is not red.
((("Harry" "is" "furry" "~")) -> ("Harry" "is" "red" "-"))
If someone is white and young then they are not quiet.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "-"))
Red, furry people are not white.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "-"))
Quiet people are not white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "-"))
Harry is not round.
True
1
proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Harry is round.
False
1
inv-proof
[(triple6)]
("Harry" "is" "round" "+")
triple6
Harry is not white.
True
2
proof
[(((triple5) -> rule8))]
("Harry" "is" "white" "-")
((triple5) -> (rule8 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Dave is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "big" "-")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule3))]
("Dave" "is" "furry" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule3))]
("Dave" "is" "furry" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not white.
True
6
proof
[(((triple2 ((triple3 ((triple3) -> rule2)) -> rule3)) -> rule7))]
("Dave" "is" "white" "-")
((triple2 ((triple3 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
False
6
inv-proof
[(((triple2 ((triple3 ((triple3) -> rule2)) -> rule3)) -> rule7))]
("Dave" "is" "white" "+")
((triple2 ((triple3 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is not quiet.[(triple1)] Dave is red.[(triple2)] Dave is young.[(triple3)] Harry is furry.[(triple4)] Harry is not round.[(triple6)] Harry is not young.[(triple7)] Harry is quiet.[(triple5)] @1: Dave is big.[(((triple3) -> rule2))] Harry is not white.[(((triple5) -> rule8))] @2: Dave is furry.[(((triple3 ((triple3) -> rule2)) -> rule3))] @3: Dave is not white.[(((triple2 ((triple3 ((triple3) -> rule2)) -> rule3)) -> rule7))]
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is not round.
("Harry" "is" "round" "-")
triple6
Harry is not young.
("Harry" "is" "young" "-")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple5) -> (rule8 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not white.
("Dave" "is" "white" "-")
((triple2 ((triple3 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3