Bob is quiet. Dave is quiet. Erin is furry. Harry is quiet. All blue things are round. If something is rough and not furry then it is round. If something is quiet then it is rough.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is rough and not furry then it is round.
((("something" "is" "rough" "+") ("something" "is" "furry" "~")) -> ("something" "is" "round" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Dave is quiet.
True
1
proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Erin is not furry.
False
1
inv-proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
Bob is rough.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "rough" "-")
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Bob is quiet.[(triple1)] Dave is quiet.[(triple2)] Erin is furry.[(triple3)] Harry is quiet.[(triple4)] @1: Bob is rough.[(((triple1) -> rule3))] Dave is rough.[(((triple2) -> rule3))] Harry is rough.[(((triple4) -> rule3))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1