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