Anne is blue. Anne is white. Anne is young. Bob is kind. Bob is quiet. Bob is not young. Dave is white. Dave is young. Fiona is quiet. Fiona is not red. Fiona is white. Fiona is not young. If something is blue then it is kind. Blue, red things are not kind. If Dave is young and Dave is not white then Dave is kind. If Dave is white and Dave is blue then Dave is not kind. Young, kind things are green. If something is red then it is young. If something is kind and green then it is quiet. If something is red then it is not quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not young.
("Bob" "is" "young" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Blue, red things are not kind.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "-"))
If Dave is young and Dave is not white then Dave is kind.
((("Dave" "is" "young" "+") ("Dave" "is" "white" "~")) -> ("Dave" "is" "kind" "+"))
If Dave is white and Dave is blue then Dave is not kind.
((("Dave" "is" "white" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "kind" "-"))
Young, kind things are green.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is kind and green then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is not quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
Bob is quiet.
True
1
proof
[(triple5)]
("Bob" "is" "quiet" "+")
triple5
Fiona is not quiet.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "quiet" "-")
triple9
Anne is kind.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
True
4
proof
[(((triple3 ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "green" "+")
((triple3 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not green.
False
4
inv-proof
[(((triple3 ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "green" "-")
((triple3 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "green" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is white.[(triple2)] Anne is young.[(triple3)] Bob is kind.[(triple4)] Bob is not young.[(triple6)] Bob is quiet.[(triple5)] Dave is white.[(triple7)] Dave is young.[(triple8)] Fiona is not red.[(triple10)] Fiona is not young.[(triple12)] Fiona is quiet.[(triple9)] Fiona is white.[(triple11)] @1: Anne is kind.[(((triple1) -> rule1))] @2: Anne is green.[(((triple3 ((triple1) -> rule1)) -> rule5))] @3: Anne is quiet.[(((((triple1) -> rule1) ((triple3 ((triple1) -> rule1)) -> rule5)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Fiona is not red.
("Fiona" "is" "red" "-")
triple10
Fiona is not young.
("Fiona" "is" "young" "-")
triple12
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple3 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int3)) ((triple3 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3