Bob is white. Charlie is green. Dave is kind. Erin is white. Nice people are white. If someone is furry then they are kind. All kind, round people are white. Kind, red people are nice. If someone is green then they are furry. All white people are red. All red people are kind. If someone is green and kind then they are furry.
Bob is white.
("Bob" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All kind, round people are white.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Kind, red people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All white people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and kind then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Erin is white.
True
1
proof
[(triple4)]
("Erin" "is" "white" "+")
triple4
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Bob is red.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "red" "+")
((triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "red" "-")
((triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule6)) -> rule7))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule7))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is nice.
True
6
proof
[(((((((triple4) -> rule6)) -> rule7) ((triple4) -> rule6)) -> rule4))]
("Erin" "is" "nice" "+")
((((((triple4) -> (rule6 % int3))) -> (rule7 % int2)) ((triple4) -> (rule6 % int3))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not nice.
False
6
inv-proof
[(((((((triple4) -> rule6)) -> rule7) ((triple4) -> rule6)) -> rule4))]
("Erin" "is" "nice" "-")
((((((triple4) -> (rule6 % int3))) -> (rule7 % int2)) ((triple4) -> (rule6 % int3))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "furry" "-")
Dave is red.
Unknown
rconc
[@3: Dave is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule4 <- FAIL)]]
("Dave" "is" "red" "+")
Charlie is not white.
Unknown
inv-rconc
[@4: Charlie is white.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule4 <- FAIL)]]
("Charlie" "is" "red" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is white.[(triple1)] Charlie is green.[(triple2)] Dave is kind.[(triple3)] Erin is white.[(triple4)] @1: Bob is red.[(((triple1) -> rule6))] Charlie is furry.[(((triple2) -> rule5))] Erin is red.[(((triple4) -> rule6))] @2: Bob is kind.[(((((triple1) -> rule6)) -> rule7))] Charlie is kind.[(((((triple2) -> rule5)) -> rule2))] Erin is kind.[(((((triple4) -> rule6)) -> rule7))] @3: Bob is nice.[(((((((triple1) -> rule6)) -> rule7) ((triple1) -> rule6)) -> rule4))] Erin is nice.[(((((((triple4) -> rule6)) -> rule7) ((triple4) -> rule6)) -> rule4))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule7 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((((triple4) -> (rule6 % int3))) -> (rule7 % int2)) ((triple4) -> (rule6 % int3))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3