Bob is not nice. Bob is rough. Harry is furry. If Harry is furry then Harry is nice. Rough, blue people are furry. Quiet people are not green. If someone is nice and not blue then they are not young. All furry people are quiet. If someone is green and not blue then they are not nice.
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Harry is furry then Harry is nice.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "nice" "+"))
Rough, blue people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Quiet people are not green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "-"))
If someone is nice and not blue then they are not young.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "-"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green and not blue then they are not nice.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "-"))
Bob is not nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Harry is not furry.
False
1
inv-proof
[(triple3)]
("Harry" "is" "furry" "-")
triple3
Harry is nice.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not green.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("Harry" "is" "green" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3))]
("Harry" "is" "green" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is not nice.[(triple1)] Bob is rough.[(triple2)] Harry is furry.[(triple3)] @1: Harry is nice.[(((triple3) -> rule1))] Harry is quiet.[(((triple3) -> rule5))] @2: Harry is not green.[(((((triple3) -> rule5)) -> rule3))]
Bob is not nice.
("Bob" "is" "nice" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2