Anne is red. Bob is rough. Dave is blue. Dave is furry. Dave is red. Harry is smart. Harry is white. All red things are rough.
Anne is red.
("Anne" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Harry is not white.
False
1
inv-proof
[(triple7)]
("Harry" "is" "white" "-")
triple7
Anne is rough.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple5) -> rule1))]
("Dave" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is red.[(triple1)] Bob is rough.[(triple2)] Dave is blue.[(triple3)] Dave is furry.[(triple4)] Dave is red.[(triple5)] Harry is smart.[(triple6)] Harry is white.[(triple7)] @1: Anne is rough.[(((triple1) -> rule1))] Dave is rough.[(((triple5) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1