Charlie is smart. Dave is rough. Harry is quiet. Furry things are quiet. Furry things are young. If something is young then it is rough. If Harry is quiet and Harry is furry then Harry is smart. Quiet things are kind. All cold things are furry. Rough things are furry. All furry things are smart.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Harry is quiet and Harry is furry then Harry is smart.
((("Harry" "is" "quiet" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "smart" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple3)]
("Harry" "is" "quiet" "-")
triple3
Dave is furry.
True
2
proof
[(((triple2) -> rule7))]
("Dave" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple2) -> rule7)) -> rule1))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule8))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
True
4
proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule5))]
("Dave" "is" "kind" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule5))]
("Dave" "is" "kind" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@4: Charlie is furry.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is young.
Unknown
rconc
[@3: Charlie is young.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule3 <- FAIL)]]
("Charlie" "is" "young" "+")
Harry is not rough.
Unknown
inv-rconc
[@3: Harry is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- FAIL)]]
("Harry" "is" "rough" "-")
Charlie is quiet.
Unknown
rconc
[@5: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule3 <- rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is smart.[(triple1)] Dave is rough.[(triple2)] Harry is quiet.[(triple3)] @1: Dave is furry.[(((triple2) -> rule7))] Harry is kind.[(((triple3) -> rule5))] @2: Dave is quiet.[(((((triple2) -> rule7)) -> rule1))] Dave is smart.[(((((triple2) -> rule7)) -> rule8))] Dave is young.[(((((triple2) -> rule7)) -> rule2))] @3: Dave is kind.[(((((((triple2) -> rule7)) -> rule1)) -> rule5))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3