Anne is quiet. Anne is white. Erin is red. Erin is smart. Fiona is red. Gary is kind. Gary is red. If Gary is smart and Gary is green then Gary is kind. If something is green and not white then it is kind. If something is white and not red then it is kind. Red things are not green. All kind things are not quiet. If Erin is not green then Erin is kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
If Gary is smart and Gary is green then Gary is kind.
((("Gary" "is" "smart" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "kind" "+"))
If something is green and not white then it is kind.
((("something" "is" "green" "+") ("something" "is" "white" "~")) -> ("something" "is" "kind" "+"))
If something is white and not red then it is kind.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "+"))
Red things are not green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
All kind things are not quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "-"))
If Erin is not green then Erin is kind.
((("Erin" "is" "green" "~")) -> ("Erin" "is" "kind" "+"))
Gary is red.
True
1
proof
[(triple7)]
("Gary" "is" "red" "+")
triple7
Fiona is not red.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "red" "-")
triple5
Gary is not green.
True
2
proof
[(((triple7) -> rule4))]
("Gary" "is" "green" "-")
((triple7) -> (rule4 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Erin is green.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is kind.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("Erin" "is" "kind" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("Erin" "is" "kind" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Erin is not quiet.
True
4
proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "quiet" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
int3
Erin is quiet.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is quiet.[(triple1)] Anne is white.[(triple2)] Erin is red.[(triple3)] Erin is smart.[(triple4)] Fiona is red.[(triple5)] Gary is kind.[(triple6)] Gary is red.[(triple7)] @1: Erin is not green.[(((triple3) -> rule4))] Fiona is not green.[(((triple5) -> rule4))] Gary is not green.[(((triple7) -> rule4))] Gary is not quiet.[(((triple6) -> rule5))] @2: Erin is kind.[(((((triple3) -> rule4)) -> rule6))] @3: Erin is not quiet.[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Erin is not green.
("Erin" "is" "green" "-")
((triple3) -> (rule4 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Fiona is not green.
("Fiona" "is" "green" "-")
((triple5) -> (rule4 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Gary is not green.
("Gary" "is" "green" "-")
((triple7) -> (rule4 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple6) -> (rule5 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Erin is not quiet.
("Erin" "is" "quiet" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
int3