Dave is blue. Dave is furry. Dave is not round. Dave is young. Harry is not big. Harry is blue. Harry is kind. If Harry is blue and Harry is big then Harry is young. If Dave is big then Dave is not young. If something is kind and not big then it is young. If Dave is smart and Dave is round then Dave is not blue. Young things are smart. If something is round and furry then it is smart. If something is big and not kind then it is round. If something is smart and not big then it is not furry.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is young.
("Dave" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Harry is blue and Harry is big then Harry is young.
((("Harry" "is" "blue" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "young" "+"))
If Dave is big then Dave is not young.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "young" "-"))
If something is kind and not big then it is young.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "young" "+"))
If Dave is smart and Dave is round then Dave is not blue.
((("Dave" "is" "smart" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "-"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is round and furry then it is smart.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is big and not kind then it is round.
((("something" "is" "big" "+") ("something" "is" "kind" "~")) -> ("something" "is" "round" "+"))
If something is smart and not big then it is not furry.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "furry" "-"))
Dave is not round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
Harry is big.
False
1
inv-proof
[(triple5)]
("Harry" "is" "big" "+")
triple5
Dave is smart.
True
2
proof
[(((triple4) -> rule5))]
("Dave" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is not young.
False
3
inv-proof
[(((triple7 triple5) -> rule3))]
("Harry" "is" "young" "-")
((triple7 triple5) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
True
4
proof
[(((((triple7 triple5) -> rule3)) -> rule5))]
("Harry" "is" "smart" "+")
((((triple7 triple5) -> (rule3 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple7 triple5) -> rule3)) -> rule5))]
("Harry" "is" "smart" "-")
((((triple7 triple5) -> (rule3 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not furry.
True
6
proof
[(((((((triple7 triple5) -> rule3)) -> rule5) triple5) -> rule8))]
("Harry" "is" "furry" "-")
((((((triple7 triple5) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is furry.
False
6
inv-proof
[(((((((triple7 triple5) -> rule3)) -> rule5) triple5) -> rule8))]
("Harry" "is" "furry" "+")
((((((triple7 triple5) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "round" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is blue.[(triple1)] Dave is furry.[(triple2)] Dave is not round.[(triple3)] Dave is young.[(triple4)] Harry is blue.[(triple6)] Harry is kind.[(triple7)] Harry is not big.[(triple5)] @1: Dave is smart.[(((triple4) -> rule5))] Harry is young.[(((triple7 triple5) -> rule3))] @2: Harry is smart.[(((((triple7 triple5) -> rule3)) -> rule5))] @3: Harry is not furry.[(((((((triple7 triple5) -> rule3)) -> rule5) triple5) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is not round.
("Dave" "is" "round" "-")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is not big.
("Harry" "is" "big" "-")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple7 triple5) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7 triple5) -> (rule3 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
((((((triple7 triple5) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3