Anne is not big. Bob is big. Erin is smart. Gary is blue. If Gary is furry then Gary is not smart. All young things are furry. If something is big then it is furry.
Anne is not big.
("Anne" "is" "big" "-")
Bob is big.
("Bob" "is" "big" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If Gary is furry then Gary is not smart.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "smart" "-"))
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Gary is blue.
True
1
proof
[(triple4)]
("Gary" "is" "blue" "+")
triple4
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Bob is furry.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "furry" "-")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is not big.[(triple1)] Bob is big.[(triple2)] Erin is smart.[(triple3)] Gary is blue.[(triple4)] @1: Bob is furry.[(((triple2) -> rule3))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1