Anne is smart. Bob is green. Gary is not blue. Kind people are young. If someone is young then they are white. Green people are white. White people are blue. If someone is blue and not young then they are furry. If someone is blue then they are furry.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is green.
("Bob" "is" "green" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and not young then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Bob is white.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "white" "+")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "white" "-")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("Bob" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
True
4
proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule6))]
("Bob" "is" "furry" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule6))]
("Bob" "is" "furry" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "white" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is smart.[(triple1)] Bob is green.[(triple2)] Gary is not blue.[(triple3)] @1: Bob is white.[(((triple2) -> rule3))] @2: Bob is blue.[(((((triple2) -> rule3)) -> rule4))] @3: Bob is furry.[(((((((triple2) -> rule3)) -> rule4)) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Gary is not blue.
("Gary" "is" "blue" "-")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3