Charlie is green. Dave is furry. Erin is not furry. Erin is quiet. Fiona is nice. Fiona is quiet. Fiona is not white. If someone is white then they are furry. All white people are not furry. Nice people are red. If someone is quiet and not nice then they are not red. If someone is furry and not white then they are green. If someone is kind and quiet then they are not green. If Dave is kind and Dave is not quiet then Dave is furry. All red people are kind.
Charlie is green.
("Charlie" "is" "green" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All white people are not furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "-"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet and not nice then they are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "-"))
If someone is furry and not white then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "+"))
If someone is kind and quiet then they are not green.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "-"))
If Dave is kind and Dave is not quiet then Dave is furry.
((("Dave" "is" "kind" "+") ("Dave" "is" "quiet" "~")) -> ("Dave" "is" "furry" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Erin is quiet.
True
1
proof
[(triple4)]
("Erin" "is" "quiet" "+")
triple4
Fiona is white.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "white" "+")
triple7
Fiona is red.
True
2
proof
[(((triple5) -> rule3))]
("Fiona" "is" "red" "+")
((triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple5) -> rule3))]
("Fiona" "is" "red" "-")
((triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
True
3
proof
[(((((triple5) -> rule3)) -> rule8))]
("Fiona" "is" "kind" "+")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not kind.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule8))]
("Fiona" "is" "kind" "-")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not green.
True
5
proof
[(((((((triple5) -> rule3)) -> rule8) triple6) -> rule6))]
("Fiona" "is" "green" "-")
((((((triple5) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is green.
False
5
inv-proof
[(((((((triple5) -> rule3)) -> rule8) triple6) -> rule6))]
("Fiona" "is" "green" "+")
((((((triple5) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is green.[(triple1)] Dave is furry.[(triple2)] Erin is not furry.[(triple3)] Erin is quiet.[(triple4)] Fiona is nice.[(triple5)] Fiona is not white.[(triple7)] Fiona is quiet.[(triple6)] @1: Fiona is red.[(((triple5) -> rule3))] @2: Fiona is kind.[(((((triple5) -> rule3)) -> rule8))] @3: Fiona is not green.[(((((((triple5) -> rule3)) -> rule8) triple6) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is not furry.
("Erin" "is" "furry" "-")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is not white.
("Fiona" "is" "white" "-")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
((triple5) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not green.
("Fiona" "is" "green" "-")
((((((triple5) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3