Dave is kind. Erin is green. Erin is quiet. Fiona is green. Fiona is kind. Fiona is quiet. Fiona is red. Quiet things are kind. Furry things are green. All kind, green things are red. If Erin is nice then Erin is kind. All white, green things are kind. Furry, nice things are quiet. If something is red then it is kind. Kind things are white.
Dave is kind.
("Dave" "is" "kind" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All kind, green things are red.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Erin is nice then Erin is kind.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "kind" "+"))
All white, green things are kind.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Furry, nice things are quiet.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Fiona is green.
True
1
proof
[(triple4)]
("Fiona" "is" "green" "+")
triple4
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Fiona is white.
True
2
proof
[(((triple5) -> rule8) OR ((((triple6) -> rule1)) -> rule8) OR ((((triple7) -> rule7)) -> rule8))]
("Fiona" "is" "white" "+")
((triple5) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "kind" "-")
((triple3) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
True
3
proof
[(((((triple3) -> rule1)) -> rule8))]
("Erin" "is" "white" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule8))]
("Erin" "is" "white" "-")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Dave is kind.[(triple1)] Erin is green.[(triple2)] Erin is quiet.[(triple3)] Fiona is green.[(triple4)] Fiona is kind.[(triple5 OR ((triple6) -> rule1) OR ((triple7) -> rule7))] Fiona is quiet.[(triple6)] Fiona is red.[(triple7 OR ((triple5 triple4) -> rule3) OR ((((triple6) -> rule1) triple4) -> rule3))] @1: Dave is white.[(((triple1) -> rule8))] Erin is kind.[(((triple3) -> rule1))] Fiona is white.[(((triple5) -> rule8) OR ((((triple6) -> rule1)) -> rule8) OR ((((triple7) -> rule7)) -> rule8))] @2: Erin is red.[(((((triple3) -> rule1) triple2) -> rule3))] Erin is white.[(((((triple3) -> rule1)) -> rule8))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
((triple6) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple7) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
((triple5 triple4) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple6) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple5) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2