Bob is furry. Charlie is quiet. Harry is rough. If someone is quiet and not blue then they are not nice. If Bob is round then Bob is furry. If someone is rough and not blue then they are furry. If someone is rough and nice then they are not furry. Round people are quiet. If Bob is rough then Bob is round. If someone is cold then they are not round. Furry people are round.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is quiet and not blue then they are not nice.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "-"))
If Bob is round then Bob is furry.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "furry" "+"))
If someone is rough and not blue then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "furry" "+"))
If someone is rough and nice then they are not furry.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is rough then Bob is round.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "round" "+"))
If someone is cold then they are not round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Bob is round.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "round" "+")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "round" "-")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule8)) -> rule5))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule5))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is quiet.
Unknown
rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule3 <- FAIL)]]
("Harry" "is" "quiet" "+")
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is furry.[(triple1)] Charlie is quiet.[(triple2)] Harry is rough.[(triple3)] @1: Bob is round.[(((triple1) -> rule8))] @2: Bob is quiet.[(((((triple1) -> rule8)) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2