Anne is round. Bob is nice. Dave is furry. Dave is nice. Dave is smart. Dave is young. Gary is smart. Smart people are young. All round people are nice. Young people are nice.
Anne is round.
("Anne" "is" "round" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Dave is young.
True
1
proof
[(triple6 OR ((triple5) -> rule1))]
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "-")
triple7
Anne is nice.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Gary is nice.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "nice" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is round.[(triple1)] Bob is nice.[(triple2)] Dave is furry.[(triple3)] Dave is nice.[(triple4 OR ((triple6) -> rule3) OR ((((triple5) -> rule1)) -> rule3))] Dave is smart.[(triple5)] Dave is young.[(triple6 OR ((triple5) -> rule1))] Gary is smart.[(triple7)] @1: Anne is nice.[(((triple1) -> rule2))] Gary is young.[(((triple7) -> rule1))] @2: Gary is nice.[(((((triple7) -> rule1)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple7) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2