Bob is quiet. Gary is furry. All quiet things are furry. If something is red and not quiet then it is round. Furry things are big.
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is red and not quiet then it is round.
((("something" "is" "red" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "round" "+"))
Furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Gary is big.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "big" "+")
((triple2) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is quiet.[(triple1)] Gary is furry.[(triple2)] @1: Bob is furry.[(((triple1) -> rule1))] Gary is big.[(((triple2) -> rule3))] @2: Bob is big.[(((((triple1) -> rule1)) -> rule3))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple2) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2