Anne is furry. Anne is kind. Bob is red. Bob is round. Charlie is blue. Charlie is red. Charlie is white. Charlie is young. Gary is blue. Gary is furry. Gary is round. Gary is not white. If Anne is furry and Anne is blue then Anne is white. If Gary is kind then Gary is not blue. If someone is furry then they are not white. If someone is kind then they are young. All young people are not round. If someone is kind and not round then they are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not white.
("Gary" "is" "white" "-")
If Anne is furry and Anne is blue then Anne is white.
((("Anne" "is" "furry" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "white" "+"))
If Gary is kind then Gary is not blue.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "-"))
If someone is furry then they are not white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "-"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All young people are not round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "-"))
If someone is kind and not round then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
Charlie is red.
True
1
proof
[(triple6)]
("Charlie" "is" "red" "+")
triple6
Charlie is not red.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "red" "-")
triple6
Anne is young.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "young" "+")
((triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is round.
False
2
inv-proof
[(((triple8) -> rule5))]
("Charlie" "is" "round" "+")
((triple8) -> (rule5 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Anne is not round.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Anne" "is" "round" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Anne" "is" "round" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not round.
("Anne" "is" "round" "-")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "red" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not round.
("Anne" "is" "round" "-")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4)] Charlie is blue.[(triple5)] Charlie is red.[(triple6)] Charlie is white.[(triple7)] Charlie is young.[(triple8)] Gary is blue.[(triple9)] Gary is furry.[(triple10)] Gary is not white.[(triple12 OR ((triple10) -> rule3))] Gary is round.[(triple11)] @1: Anne is not white.[(((triple1) -> rule3))] Anne is young.[(((triple2) -> rule4))] Charlie is not round.[(((triple8) -> rule5))] @2: Anne is not round.[(((((triple2) -> rule4)) -> rule5))] @3: Anne is red.[(((triple2 ((((triple2) -> rule4)) -> rule5)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is not white.
("Gary" "is" "white" "-")
triple12
((triple10) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
triple11
Anne is not white.
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
((triple8) -> (rule5 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Anne is not round.
("Anne" "is" "round" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not round.
("Anne" "is" "round" "-")
int2
Anne is young.
("Anne" "is" "young" "+")
int3