Bob is nice. Dave is furry. Dave is quiet. Dave is white. Gary is rough. Gary is smart. Harry is furry. Quiet things are nice. All smart things are rough. If Dave is white then Dave is smart.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Dave is white then Dave is smart.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "+")
triple6
Gary is not rough.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule2))]
("Gary" "is" "rough" "-")
triple5
((triple6) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is smart.
True
2
proof
[(((triple4) -> rule3))]
("Dave" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple4) -> rule3))]
("Dave" "is" "smart" "-")
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Dave is furry.[(triple2)] Dave is quiet.[(triple3)] Dave is white.[(triple4)] Gary is rough.[(triple5 OR ((triple6) -> rule2))] Gary is smart.[(triple6)] Harry is furry.[(triple7)] @1: Dave is nice.[(((triple3) -> rule1))] Dave is smart.[(((triple4) -> rule3))] @2: Dave is rough.[(((((triple4) -> rule3)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple6) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2