Erin is white. Fiona is kind. Fiona is round. Kind people are quiet. All white, kind people are blue. If Fiona is red then Fiona is kind. If someone is white then they are quiet. If someone is quiet then they are kind. If someone is blue and white then they are quiet. All round, white people are blue. Red people are quiet.
Erin is white.
("Erin" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All white, kind people are blue.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Fiona is red then Fiona is kind.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "kind" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and white then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All round, white people are blue.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Erin is white.
True
1
proof
[(triple1)]
("Erin" "is" "white" "+")
triple1
Fiona is not kind.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "kind" "-")
triple2
Erin is quiet.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Erin" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Erin" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule5)) -> rule2))]
("Erin" "is" "blue" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule5)) -> rule2))]
("Erin" "is" "blue" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Erin is white.[(triple1)] Fiona is kind.[(triple2)] Fiona is round.[(triple3)] @1: Erin is quiet.[(((triple1) -> rule4))] Fiona is quiet.[(((triple2) -> rule1))] @2: Erin is kind.[(((((triple1) -> rule4)) -> rule5))] @3: Erin is blue.[(((triple1 ((((triple1) -> rule4)) -> rule5)) -> rule2))]
Erin is white.
("Erin" "is" "white" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3