Anne is young. Bob is young. Dave is cold. Gary is furry. Young things are green. If something is green and young then it is furry.
Anne is young.
("Anne" "is" "young" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is green and young then it is furry.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Dave is cold.
True
1
proof
[(triple3)]
("Dave" "is" "cold" "+")
triple3
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Bob is green.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "green" "+")
((triple2) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is young.[(triple1)] Bob is young.[(triple2)] Dave is cold.[(triple3)] Gary is furry.[(triple4)] @1: Anne is green.[(((triple1) -> rule1))] Bob is green.[(((triple2) -> rule1))] @2: Anne is furry.[(((((triple1) -> rule1) triple1) -> rule2))] Bob is furry.[(((((triple2) -> rule1) triple2) -> rule2))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2