Anne is furry. Bob is smart. Harry is not furry. If Bob is nice and Bob is furry then Bob is green. If Harry is nice then Harry is green. Furry things are round. Kind, smart things are round. All round things are green. If Anne is not kind and Anne is not round then Anne is nice.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
If Bob is nice and Bob is furry then Bob is green.
((("Bob" "is" "nice" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "green" "+"))
If Harry is nice then Harry is green.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "green" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Kind, smart things are round.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If Anne is not kind and Anne is not round then Anne is nice.
((("Anne" "is" "kind" "~") ("Anne" "is" "round" "~")) -> ("Anne" "is" "nice" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Harry is furry.
False
1
inv-proof
[(triple3)]
("Harry" "is" "furry" "+")
triple3
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 green.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "nice" "+")
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Bob is smart.[(triple2)] Harry is not furry.[(triple3)] @1: Anne is round.[(((triple1) -> rule3))] @2: Anne is green.[(((((triple1) -> rule3)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Harry is not furry.
("Harry" "is" "furry" "-")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2