Anne is furry. Anne is red. Charlie is not furry. Charlie is green. Charlie is young. Fiona is quiet. Gary is green. If something is furry and blue then it is not kind. If something is furry then it is kind. All furry things are kind. All kind things are quiet. Furry, kind things are young. If something is furry and not young then it is green. If something is blue and young then it is green. Quiet, red things are green.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
If something is furry and blue then it is not kind.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Furry, kind things are young.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is furry and not young then it is green.
((("something" "is" "furry" "+") ("something" "is" "young" "~")) -> ("something" "is" "green" "+"))
If something is blue and young then it is green.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Quiet, red things are green.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Fiona is quiet.
True
1
proof
[(triple6)]
("Fiona" "is" "quiet" "+")
triple6
Fiona is not quiet.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "quiet" "-")
triple6
Anne is kind.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("Anne" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule4) OR ((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule5) OR ((triple1 ((triple1) -> rule3)) -> rule5))]
("Anne" "is" "young" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
True
5
proof
[(((((((triple1) -> rule2)) -> rule4) triple2) -> rule8) OR ((((((triple1) -> rule3)) -> rule4) triple2) -> rule8))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not green.
False
5
inv-proof
[(((((((triple1) -> rule2)) -> rule4) triple2) -> rule8) OR ((((((triple1) -> rule3)) -> rule4) triple2) -> rule8))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "young" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2)] Charlie is green.[(triple4)] Charlie is not furry.[(triple3)] Charlie is young.[(triple5)] Fiona is quiet.[(triple6)] Gary is green.[(triple7)] @1: Anne is kind.[(((triple1) -> rule2) OR ((triple1) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule2)) -> rule4) OR ((((triple1) -> rule3)) -> rule4))] Anne is young.[(((triple1 ((triple1) -> rule2)) -> rule5) OR ((triple1 ((triple1) -> rule3)) -> rule5))] @3: Anne is green.[(((((((triple1) -> rule2)) -> rule4) triple2) -> rule8) OR ((((((triple1) -> rule3)) -> rule4) triple2) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3