Bob is furry. Gary is big. Gary is quiet. All nice people are not quiet. If Bob is furry then Bob is nice. All quiet people are green. If Bob is not green then Bob is big. All furry people are not big. If someone is green and not quiet then they are big.
Bob is furry.
("Bob" "is" "furry" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All nice people are not quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "-"))
If Bob is furry then Bob is nice.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Bob is not green then Bob is big.
((("Bob" "is" "green" "~")) -> ("Bob" "is" "big" "+"))
All furry people are not big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "-"))
If someone is green and not quiet then they are big.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "+"))
Gary is big.
True
1
proof
[(triple2)]
("Gary" "is" "big" "+")
triple2
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Gary is green.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "green" "+")
((triple3) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is not quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is furry.[(triple1)] Gary is big.[(triple2)] Gary is quiet.[(triple3)] @1: Bob is nice.[(((triple1) -> rule2))] Bob is not big.[(((triple1) -> rule5))] Gary is green.[(((triple3) -> rule3))] @2: Bob is not quiet.[(((((triple1) -> rule2)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not big.
("Bob" "is" "big" "-")
((triple1) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2