Anne is rough. Bob is nice. Dave is smart. Harry is quiet. Round, rough things are quiet. Furry, quiet things are nice. If something is rough then it is round.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Round, rough things are quiet.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Furry, quiet things are nice.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "-")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not quiet.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is rough.[(triple1)] Bob is nice.[(triple2)] Dave is smart.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is round.[(((triple1) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule3) triple1) -> rule1))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2