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