Bob is furry. Charlie is nice. Dave is nice. Gary is red. Quiet, kind people are red. If someone is quiet then they are furry. All quiet people are nice. Nice people are young. Young, nice people are rough. All furry people are kind.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Young, nice people are rough.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple4)]
("Gary" "is" "red" "-")
triple4
Dave is young.
True
2
proof
[(((triple3) -> rule4))]
("Dave" "is" "young" "+")
((triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "kind" "-")
((triple1) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Bob is young.
Unknown
rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Bob" "is" "young" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Bob is furry.[(triple1)] Charlie is nice.[(triple2)] Dave is nice.[(triple3)] Gary is red.[(triple4)] @1: Bob is kind.[(((triple1) -> rule6))] Charlie is young.[(((triple2) -> rule4))] Dave is young.[(((triple3) -> rule4))] @2: Charlie is rough.[(((((triple2) -> rule4) triple2) -> rule5))] Dave is rough.[(((((triple3) -> rule4) triple3) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2