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