Anne is red. Bob is big. Charlie is kind. Gary is quiet. All young, kind things are furry. Rough, red things are kind. If something is rough and big then it is furry. If something is red and young then it is quiet. If something is red then it is furry. If Anne is furry then Anne is young.
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All young, kind things are furry.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Rough, red things are kind.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is rough and big then it is furry.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is red and young then it is quiet.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Anne is furry then Anne is young.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "young" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "young" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule6)) -> rule4))]
("Anne" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not quiet.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule6)) -> rule4))]
("Anne" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is red.[(triple1)] Bob is big.[(triple2)] Charlie is kind.[(triple3)] Gary is quiet.[(triple4)] @1: Anne is furry.[(((triple1) -> rule5))] @2: Anne is young.[(((((triple1) -> rule5)) -> rule6))] @3: Anne is quiet.[(((triple1 ((((triple1) -> rule5)) -> rule6)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3