Bob is furry. Gary is not round. Harry is quiet. If Harry is quiet then Harry is furry. Red things are not quiet. If something is furry then it is rough. All quiet things are furry. If Harry is nice then Harry is not quiet. If Bob is not furry then Bob is rough.
Bob is furry.
("Bob" "is" "furry" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is quiet then Harry is furry.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "furry" "+"))
Red things are not quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Harry is nice then Harry is not quiet.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "-"))
If Bob is not furry then Bob is rough.
((("Bob" "is" "furry" "~")) -> ("Bob" "is" "rough" "+"))
Gary is not round.
True
1
proof
[(triple2)]
("Gary" "is" "round" "-")
triple2
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is rough.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple3) -> rule4))]
("Harry" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule4)) -> rule3))]
("Harry" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule4)) -> rule3))]
("Harry" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is furry.[(triple1)] Gary is not round.[(triple2)] Harry is quiet.[(triple3)] @1: Bob is rough.[(((triple1) -> rule3))] Harry is furry.[(((triple3) -> rule1) OR ((triple3) -> rule4))] @2: Harry is rough.[(((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule4)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Gary is not round.
("Gary" "is" "round" "-")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2